| (* |
| * Copyright 2016, NICTA |
| * |
| * This software may be distributed and modified according to the terms of |
| * the GNU General Public License version 2. Note that NO WARRANTY is provided. |
| * See "LICENSE_GPLv2.txt" for details. |
| * |
| * @TAG(NICTA_GPL) |
| *) |
| |
| (* |
| * Program specifications generated from: |
| * cd bilby/cogent/tests/antiquote-tests/test-wordarray |
| * cogent --fno-tuple-as-sugar --type-proof=WordArrayTest wordarray_simple_nodebug.cogent > WordArrayTest.thy |
| * make SRC=wordarray_simple_nodebug.cogent && cp main_pp_inferred.c wordarraytest.c |
| *) |
| theory WordArrayTest |
| imports |
| "../TypeProofGen" |
| "../Cogent_Corres" |
| "../Read_Table" |
| "../Type_Relation_Generation" |
| begin |
| |
| definition |
| "abbreviatedType1 \<equiv> TSum [(''Error'', TUnit), (''Success'', TPrim (Num U64))]" |
| |
| definition |
| "abbreviatedType2 \<equiv> TSum [(''Error'', TUnit), (''Success'', TPrim (Num U32))]" |
| |
| lemmas abbreviated_type_defs = |
| abbreviatedType2_def |
| abbreviatedType1_def |
| |
| definition |
| "u8_to_u64_type \<equiv> ([], (TPrim (Num U8), TPrim (Num U64)))" |
| |
| definition |
| "u8_to_u32_type \<equiv> ([], (TPrim (Num U8), TPrim (Num U32)))" |
| |
| definition |
| "u8_to_u16_type \<equiv> ([], (TPrim (Num U8), TPrim (Num U16)))" |
| |
| definition |
| "u64_to_u32_type \<equiv> ([], (TPrim (Num U64), TPrim (Num U32)))" |
| |
| definition |
| "u32_to_u8_type \<equiv> ([], (TPrim (Num U32), TPrim (Num U8)))" |
| |
| definition |
| "u32_to_u64_type \<equiv> ([], (TPrim (Num U32), TPrim (Num U64)))" |
| |
| definition |
| "u32_to_u16_type \<equiv> ([], (TPrim (Num U32), TPrim (Num U16)))" |
| |
| definition |
| "u16_to_u8_type \<equiv> ([], (TPrim (Num U16), TPrim (Num U8)))" |
| |
| definition |
| "u16_to_u32_type \<equiv> ([], (TPrim (Num U16), TPrim (Num U32)))" |
| |
| definition |
| "test_time_start_type \<equiv> ([], (TUnit, TUnit))" |
| |
| definition |
| "test_time_end_type \<equiv> ([], (TUnit, TUnit))" |
| |
| definition |
| "test_stack_probe_type \<equiv> ([], (TUnit, TUnit))" |
| |
| definition |
| "random_u32_type \<equiv> ([], (TUnit, TPrim (Num U32)))" |
| |
| definition |
| "cogent_log2_type \<equiv> ([], (TPrim (Num U32), TPrim (Num U32)))" |
| |
| definition |
| "wordarray_cmp_type \<equiv> ([], (TProduct (TCon ''WordArray'' [TPrim (Num U8)] ReadOnly) (TCon ''WordArray'' [TPrim (Num U8)] ReadOnly), TPrim Bool))" |
| |
| definition |
| "wordarray_get_0_type \<equiv> ([], (TProduct (TCon ''WordArray'' [TPrim (Num U32)] ReadOnly) (TPrim (Num U32)), TPrim (Num U32)))" |
| |
| definition |
| "wordarray_put_0_type \<equiv> ([], (TRecord [(TCon ''WordArray'' [TPrim (Num U32)] Writable, False), (TPrim (Num U32), False), (TPrim (Num U32), False)] Unboxed, TSum [(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable), (''Success'', TCon ''WordArray'' [TPrim (Num U32)] Writable)]))" |
| |
| definition |
| "test_file_read_next_u32_type \<equiv> ([], (TCon ''File'' [] Writable, TSum [(''Error'', TCon ''File'' [] Writable), (''Success'', TProduct (TCon ''File'' [] Writable) (TPrim (Num U32)))]))" |
| |
| definition |
| "test_file_close_type \<equiv> ([], (TProduct (TCon ''SysState'' [] Writable) (TCon ''File'' [] Writable), TCon ''SysState'' [] Writable))" |
| |
| definition |
| "test_file_open_type \<equiv> ([], (TProduct (TCon ''SysState'' [] Writable) (TProduct (TPrim String) (TPrim String)), TSum [(''Error'', TCon ''SysState'' [] Writable), (''Success'', TProduct (TCon ''SysState'' [] Writable) (TCon ''File'' [] Writable))]))" |
| |
| definition |
| "wordarray_create_0_type \<equiv> ([], (TProduct (TCon ''SysState'' [] Writable) (TPrim (Num U32)), TSum [(''Error'', TCon ''SysState'' [] Writable), (''Success'', TProduct (TCon ''SysState'' [] Writable) (TCon ''WordArray'' [TPrim (Num U32)] Writable))]))" |
| |
| definition |
| "wordarray_free_0_type \<equiv> ([], (TProduct (TCon ''SysState'' [] Writable) (TCon ''WordArray'' [TPrim (Num U32)] Writable), TCon ''SysState'' [] Writable))" |
| |
| definition |
| "u16_to_u64_type \<equiv> ([], (TPrim (Num U16), TPrim (Num U64)))" |
| |
| definition |
| "u16_to_u64 \<equiv> Let (Var 0) (Let (App (AFun ''u16_to_u32'' []) (Var 0)) (App (AFun ''u32_to_u64'' []) (Var 0)))" |
| |
| definition |
| "min_u32_type \<equiv> ([], (TProduct (TPrim (Num U32)) (TPrim (Num U32)), TPrim (Num U32)))" |
| |
| definition |
| "min_u32 \<equiv> Split (Var 0) (Let (Prim (Lt U32) [Var 0, Var 1]) (If (Var 0) (Var 1) (Var 2)))" |
| |
| definition |
| "cogent_low_16_bits_type \<equiv> ([], (TPrim (Num U32), TPrim (Num U16)))" |
| |
| definition |
| "cogent_low_16_bits \<equiv> Let (Var 0) (Let (Lit (LU16 65535)) (Let (Cast U32 (Var 0)) (Let (Prim (BitAnd U32) [Var 2, Var 0]) (App (AFun ''u32_to_u16'' []) (Var 0)))))" |
| |
| definition |
| "cogent_high_16_bits_type \<equiv> ([], (TPrim (Num U32), TPrim (Num U16)))" |
| |
| definition |
| "cogent_high_16_bits \<equiv> Let (Var 0) (Let (Lit (LU32 4294901760)) (Let (Prim (BitAnd U32) [Var 1, Var 0]) (Let (Lit (LU8 16)) (Let (App (AFun ''u8_to_u32'' []) (Var 0)) (Let (Prim (RShift U32) [Var 2, Var 0]) (App (AFun ''u32_to_u16'' []) (Var 0)))))))" |
| |
| definition |
| "align64_type \<equiv> ([], (TProduct (TPrim (Num U64)) (TPrim (Num U64)), TPrim (Num U64)))" |
| |
| definition |
| "align64 \<equiv> Split (Var 0) (Let (Prim (Mod U64) [Var 0, Var 1]) (Let (Lit (LU8 0)) (Let (Cast U64 (Var 0)) (Let (Prim (NEq (Num U64)) [Var 2, Var 0]) (If (Var 0) (Let (Prim (Plus U64) [Var 4, Var 5]) (Let (Prim (Mod U64) [Var 5, Var 6]) (Prim (Minus U64) [Var 1, Var 0]))) (Var 4))))))" |
| |
| definition |
| "align32_type \<equiv> ([], (TProduct (TPrim (Num U32)) (TPrim (Num U32)), TPrim (Num U32)))" |
| |
| definition |
| "align32 \<equiv> Split (Var 0) (Let (Prim (Mod U32) [Var 0, Var 1]) (Let (Lit (LU8 0)) (Let (Cast U32 (Var 0)) (Let (Prim (NEq (Num U32)) [Var 2, Var 0]) (If (Var 0) (Let (Prim (Plus U32) [Var 4, Var 5]) (Let (Prim (Mod U32) [Var 5, Var 6]) (Prim (Minus U32) [Var 1, Var 0]))) (Var 4))))))" |
| |
| definition |
| "safe_add32_type \<equiv> ([], (TProduct (TPrim (Num U32)) (TPrim (Num U32)), abbreviatedType2))" |
| |
| definition |
| "safe_add32 \<equiv> Split (Var 0) (Let (Prim (Plus U32) [Var 0, Var 1]) (Let (Prim (Lt U32) [Var 0, Var 1]) (Let (Prim (Lt U32) [Var 1, Var 3]) (Let (Prim Cogent.Or [Var 1, Var 0]) (If (Var 0) (Let Unit (Let (Con [(''Error'', TUnit)] ''Error'' (Var 0)) (Promote [(''Error'', TUnit), (''Success'', TPrim (Num U32))] (Var 0)))) (Let (Con [(''Success'', TPrim (Num U32))] ''Success'' (Var 3)) (Promote [(''Error'', TUnit), (''Success'', TPrim (Num U32))] (Var 0))))))))" |
| |
| definition |
| "safe_add64_type \<equiv> ([], (TProduct (TPrim (Num U64)) (TPrim (Num U64)), abbreviatedType1))" |
| |
| definition |
| "safe_add64 \<equiv> Split (Var 0) (Let (Prim (Plus U64) [Var 0, Var 1]) (Let (Prim (Lt U64) [Var 0, Var 1]) (Let (Prim (Lt U64) [Var 1, Var 3]) (Let (Prim Cogent.Or [Var 1, Var 0]) (If (Var 0) (Let Unit (Let (Con [(''Error'', TUnit)] ''Error'' (Var 0)) (Promote [(''Error'', TUnit), (''Success'', TPrim (Num U64))] (Var 0)))) (Let (Con [(''Success'', TPrim (Num U64))] ''Success'' (Var 3)) (Promote [(''Error'', TUnit), (''Success'', TPrim (Num U64))] (Var 0))))))))" |
| |
| definition |
| "safe_sub32_type \<equiv> ([], (TProduct (TPrim (Num U32)) (TPrim (Num U32)), abbreviatedType2))" |
| |
| definition |
| "safe_sub32 \<equiv> Split (Var 0) (Let (Prim (Minus U32) [Var 0, Var 1]) (Let (Prim (Gt U32) [Var 0, Var 1]) (If (Var 0) (Let Unit (Let (Con [(''Error'', TUnit)] ''Error'' (Var 0)) (Promote [(''Error'', TUnit), (''Success'', TPrim (Num U32))] (Var 0)))) (Let (Con [(''Success'', TPrim (Num U32))] ''Success'' (Var 1)) (Promote [(''Error'', TUnit), (''Success'', TPrim (Num U32))] (Var 0))))))" |
| |
| definition |
| "safe_sub64_type \<equiv> ([], (TProduct (TPrim (Num U64)) (TPrim (Num U64)), abbreviatedType1))" |
| |
| definition |
| "safe_sub64 \<equiv> Split (Var 0) (Let (Prim (Minus U64) [Var 0, Var 1]) (Let (Prim (Gt U64) [Var 0, Var 1]) (If (Var 0) (Let Unit (Let (Con [(''Error'', TUnit)] ''Error'' (Var 0)) (Promote [(''Error'', TUnit), (''Success'', TPrim (Num U64))] (Var 0)))) (Let (Con [(''Success'', TPrim (Num U64))] ''Success'' (Var 1)) (Promote [(''Error'', TUnit), (''Success'', TPrim (Num U64))] (Var 0))))))" |
| |
| definition |
| "caller_type \<equiv> ([], (TCon ''SysState'' [] Writable, TCon ''SysState'' [] Writable))" |
| |
| definition |
| "caller \<equiv> Let (Var 0) (Let (Lit (LU8 4)) (Let (Cast U32 (Var 0)) (Let (Tuple (Var 2) (Var 0)) (Let (App (AFun ''wordarray_create_0'' []) (Var 0)) (Case (Var 0) ''Success'' (Split (Var 0) (Let (Lit (LU8 0)) (Let (App (AFun ''u8_to_u32'' []) (Var 0)) (Let (Lit (LU8 42)) (Let (App (AFun ''u8_to_u32'' []) (Var 0)) (Let (Struct [TCon ''WordArray'' [TPrim (Num U32)] Writable, TPrim (Num U32), TPrim (Num U32)] [Var 5, Var 2, Var 0]) (Let (App (AFun ''wordarray_put_0'' []) (Var 0)) (Case (Var 0) ''Success'' (LetBang (set [0]) (Let (Lit (LU8 0)) (Let (Cast U32 (Var 0)) (Let (Tuple (Var 2) (Var 0)) (App (AFun ''wordarray_get_0'' []) (Var 0))))) (Let (Tuple (Var 8) (Var 1)) (App (AFun ''wordarray_free_0'' []) (Var 0)))) (Let (Esac (Var 0)) (Let (Tuple (Var 8) (Var 0)) (App (AFun ''wordarray_free_0'' []) (Var 0)))))))))))) (Let (Esac (Var 0)) (Var 0)))))))" |
| |
| definition |
| "\<Xi> func_name' \<equiv> case func_name' of ''u8_to_u64'' \<Rightarrow> u8_to_u64_type | ''u8_to_u32'' \<Rightarrow> u8_to_u32_type | ''u8_to_u16'' \<Rightarrow> u8_to_u16_type | ''u64_to_u32'' \<Rightarrow> u64_to_u32_type | ''u32_to_u8'' \<Rightarrow> u32_to_u8_type | ''u32_to_u64'' \<Rightarrow> u32_to_u64_type | ''u32_to_u16'' \<Rightarrow> u32_to_u16_type | ''u16_to_u8'' \<Rightarrow> u16_to_u8_type | ''u16_to_u32'' \<Rightarrow> u16_to_u32_type | ''test_time_start'' \<Rightarrow> test_time_start_type | ''test_time_end'' \<Rightarrow> test_time_end_type | ''test_stack_probe'' \<Rightarrow> test_stack_probe_type | ''random_u32'' \<Rightarrow> random_u32_type | ''cogent_log2'' \<Rightarrow> cogent_log2_type | ''wordarray_cmp'' \<Rightarrow> wordarray_cmp_type | ''wordarray_get_0'' \<Rightarrow> wordarray_get_0_type | ''wordarray_put_0'' \<Rightarrow> wordarray_put_0_type | ''test_file_read_next_u32'' \<Rightarrow> test_file_read_next_u32_type | ''test_file_close'' \<Rightarrow> test_file_close_type | ''test_file_open'' \<Rightarrow> test_file_open_type | ''wordarray_create_0'' \<Rightarrow> wordarray_create_0_type | ''wordarray_free_0'' \<Rightarrow> wordarray_free_0_type | ''u16_to_u64'' \<Rightarrow> u16_to_u64_type | ''min_u32'' \<Rightarrow> min_u32_type | ''cogent_low_16_bits'' \<Rightarrow> cogent_low_16_bits_type | ''cogent_high_16_bits'' \<Rightarrow> cogent_high_16_bits_type | ''align64'' \<Rightarrow> align64_type | ''align32'' \<Rightarrow> align32_type | ''safe_add32'' \<Rightarrow> safe_add32_type | ''safe_add64'' \<Rightarrow> safe_add64_type | ''safe_sub32'' \<Rightarrow> safe_sub32_type | ''safe_sub64'' \<Rightarrow> safe_sub64_type | ''caller'' \<Rightarrow> caller_type" |
| |
| definition |
| "u16_to_u64_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_L) (Cons None [])) [] TyTrLeaf [Some (TPrim (Num U32))] TyTrLeaf)" |
| |
| definition |
| "min_u32_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U32)), Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons None []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 3 None) [])) [] TyTrLeaf [] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons None [])))) [] TyTrLeaf [] TyTrLeaf)))" |
| |
| definition |
| "cogent_low_16_bits_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (append (replicate 2 None) []) [] TyTrLeaf [Some (TPrim (Num U16))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U32))] TyTrLeaf)))" |
| |
| definition |
| "cogent_high_16_bits_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (append (replicate 2 None) []) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (Cons None []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (append (replicate 4 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 4 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 3 None) [])))) [] TyTrLeaf [Some (TPrim (Num U32))] TyTrLeaf)))))" |
| |
| definition |
| "align64_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U64)), Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons None []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (append (replicate 4 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 4 None) [])) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 3 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 6 None) [])) [] TyTrLeaf [] (TyTrSplit (append (replicate 4 None) (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons None [])))) [] (TyTrSplit (append (replicate 4 None) (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (append (replicate 5 None) (Cons (Some TSK_L) (Cons (Some TSK_L) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U64))] TyTrLeaf)) [] TyTrLeaf))))))" |
| |
| definition |
| "align32_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U32)), Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons None []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (append (replicate 4 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 4 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 3 None) [])))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 6 None) [])) [] TyTrLeaf [] (TyTrSplit (append (replicate 4 None) (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons None [])))) [] (TyTrSplit (append (replicate 4 None) (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (append (replicate 5 None) (Cons (Some TSK_L) (Cons (Some TSK_L) (Cons None [])))) [] TyTrLeaf [Some (TPrim (Num U32))] TyTrLeaf)) [] TyTrLeaf))))))" |
| |
| definition |
| "safe_add32_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U32)), Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons None []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 2 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons None (Cons (Some TSK_L) (Cons None []))))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 4 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 6 None) [])) [] TyTrLeaf [] (TyTrSplit (append (replicate 3 None) (Cons (Some TSK_S) (append (replicate 3 None) []))) [] (TyTrSplit (append (replicate 3 None) (Cons (Some TSK_L) (append (replicate 3 None) []))) [] TyTrLeaf [Some TUnit] (TyTrSplit (Cons (Some TSK_L) (append (replicate 7 None) [])) [] TyTrLeaf [Some (TSum [(''Error'', TUnit)])] TyTrLeaf)) [] (TyTrSplit (append (replicate 3 None) (Cons (Some TSK_L) (append (replicate 3 None) []))) [] TyTrLeaf [Some (TSum [(''Success'', TPrim (Num U32))])] TyTrLeaf)))))))" |
| |
| definition |
| "safe_add64_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U64)), Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_S) (Cons None []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 2 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons None (Cons (Some TSK_S) (Cons None (Cons (Some TSK_L) (Cons None []))))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 4 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 6 None) [])) [] TyTrLeaf [] (TyTrSplit (append (replicate 3 None) (Cons (Some TSK_S) (append (replicate 3 None) []))) [] (TyTrSplit (append (replicate 3 None) (Cons (Some TSK_L) (append (replicate 3 None) []))) [] TyTrLeaf [Some TUnit] (TyTrSplit (Cons (Some TSK_L) (append (replicate 7 None) [])) [] TyTrLeaf [Some (TSum [(''Error'', TUnit)])] TyTrLeaf)) [] (TyTrSplit (append (replicate 3 None) (Cons (Some TSK_L) (append (replicate 3 None) []))) [] TyTrLeaf [Some (TSum [(''Success'', TPrim (Num U64))])] TyTrLeaf)))))))" |
| |
| definition |
| "safe_sub32_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U32)), Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (Cons None []))) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 2 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 4 None) [])) [] TyTrLeaf [] (TyTrSplit (Cons None (Cons (Some TSK_S) (append (replicate 3 None) []))) [] (TyTrSplit (Cons None (Cons (Some TSK_L) (append (replicate 3 None) []))) [] TyTrLeaf [Some TUnit] (TyTrSplit (Cons (Some TSK_L) (append (replicate 5 None) [])) [] TyTrLeaf [Some (TSum [(''Error'', TUnit)])] TyTrLeaf)) [] (TyTrSplit (Cons None (Cons (Some TSK_L) (append (replicate 3 None) []))) [] TyTrLeaf [Some (TSum [(''Success'', TPrim (Num U32))])] TyTrLeaf)))))" |
| |
| definition |
| "safe_sub64_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TPrim (Num U64)), Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (Cons None []))) [] TyTrLeaf [Some (TPrim (Num U64))] (TyTrSplit (Cons (Some TSK_S) (Cons (Some TSK_L) (append (replicate 2 None) []))) [] TyTrLeaf [Some (TPrim Bool)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 4 None) [])) [] TyTrLeaf [] (TyTrSplit (Cons None (Cons (Some TSK_S) (append (replicate 3 None) []))) [] (TyTrSplit (Cons None (Cons (Some TSK_L) (append (replicate 3 None) []))) [] TyTrLeaf [Some TUnit] (TyTrSplit (Cons (Some TSK_L) (append (replicate 5 None) [])) [] TyTrLeaf [Some (TSum [(''Error'', TUnit)])] TyTrLeaf)) [] (TyTrSplit (Cons None (Cons (Some TSK_L) (append (replicate 3 None) []))) [] TyTrLeaf [Some (TSum [(''Success'', TPrim (Num U64))])] TyTrLeaf)))))" |
| |
| definition |
| "caller_typetree \<equiv> TyTrSplit (Cons (Some TSK_L) []) [] TyTrLeaf [Some (TCon ''SysState'' [] Writable)] (TyTrSplit (append (replicate 2 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 2 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (Cons None [])))) [] TyTrLeaf [Some (TProduct (TCon ''SysState'' [] Writable) (TPrim (Num U32)))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 4 None) [])) [] TyTrLeaf [Some (TSum [(''Error'', TCon ''SysState'' [] Writable), (''Success'', TProduct (TCon ''SysState'' [] Writable) (TCon ''WordArray'' [TPrim (Num U32)] Writable))])] (TyTrSplit (Cons (Some TSK_L) (append (replicate 5 None) [])) [] TyTrLeaf [] (TyTrSplit (append (replicate 6 None) []) [Some (TProduct (TCon ''SysState'' [] Writable) (TCon ''WordArray'' [TPrim (Num U32)] Writable))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 6 None) [])) [] TyTrLeaf [Some (TCon ''SysState'' [] Writable), Some (TCon ''WordArray'' [TPrim (Num U32)] Writable)] (TyTrSplit (append (replicate 9 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 9 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (append (replicate 11 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 11 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 2 None) (Cons (Some TSK_L) (append (replicate 7 None) [])))))) [] TyTrLeaf [Some (TRecord [(TCon ''WordArray'' [TPrim (Num U32)] Writable, False), (TPrim (Num U32), False), (TPrim (Num U32), False)] Unboxed)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 13 None) [])) [] TyTrLeaf [Some (TSum [(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable), (''Success'', TCon ''WordArray'' [TPrim (Num U32)] Writable)])] (TyTrSplit (Cons (Some TSK_L) (append (replicate 14 None) [])) [] TyTrLeaf [] (TyTrSplit (append (replicate 6 None) (Cons (Some TSK_S) (append (replicate 8 None) []))) [Some (TCon ''WordArray'' [TPrim (Num U32)] Writable)] (TyTrSplit (Cons (Some TSK_NS) (append (replicate 15 None) [])) [] (TyTrSplit (append (replicate 16 None) []) [] TyTrLeaf [Some (TPrim (Num U8))] (TyTrSplit (Cons (Some TSK_L) (append (replicate 16 None) [])) [] TyTrLeaf [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons None (Cons (Some TSK_L) (append (replicate 15 None) [])))) [] TyTrLeaf [Some (TProduct (TCon ''WordArray'' [TPrim (Num U32)] ReadOnly) (TPrim (Num U32)))] TyTrLeaf))) [Some (TPrim (Num U32))] (TyTrSplit (Cons (Some TSK_L) (Cons (Some TSK_L) (append (replicate 6 None) (Cons (Some TSK_L) (append (replicate 8 None) []))))) [] TyTrLeaf [Some (TProduct (TCon ''SysState'' [] Writable) (TCon ''WordArray'' [TPrim (Num U32)] Writable))] TyTrLeaf)) [Some (TSum [(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable)])] (TyTrSplit (Cons (Some TSK_L) (append (replicate 15 None) [])) [] TyTrLeaf [Some (TCon ''WordArray'' [TPrim (Num U32)] Writable)] (TyTrSplit (Cons (Some TSK_L) (append (replicate 7 None) (Cons (Some TSK_L) (append (replicate 8 None) [])))) [] TyTrLeaf [Some (TProduct (TCon ''SysState'' [] Writable) (TCon ''WordArray'' [TPrim (Num U32)] Writable))] TyTrLeaf))))))))))) [Some (TSum [(''Error'', TCon ''SysState'' [] Writable)])] (TyTrSplit (Cons (Some TSK_L) (append (replicate 6 None) [])) [] TyTrLeaf [Some (TCon ''SysState'' [] Writable)] TyTrLeaf)))))))" |
| |
| ML {* open TTyping_Tactics *} |
| |
| ML {* |
| val typing_helper_1_script : tac list = [ |
| (RTac @{thm kind_tprim[where k = "{E,S,D}"]}) |
| ] *} |
| |
| |
| lemma typing_helper_1[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim (Num U16)) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_1_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_2_script : tac list = [ |
| (SimpTac ([],[(nth @{thms HOL.simp_thms} (25-1)),(nth @{thms HOL.simp_thms} (26-1))])) |
| ] *} |
| |
| |
| lemma typing_helper_2[unfolded abbreviated_type_defs] : |
| "list_all2 (kinding []) [] []" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_2_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_3_script : tac list = [ |
| (RTac @{thm kind_tprim[where k = "{E,S,D}"]}) |
| ] *} |
| |
| |
| lemma typing_helper_3[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim (Num U32)) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_3_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_4_script : tac list = [ |
| (RTac @{thm kind_tfun[where k = "{E,S,D}"]}), |
| (RTac @{thm typing_helper_1}), |
| (RTac @{thm typing_helper_3}) |
| ] *} |
| |
| |
| lemma typing_helper_4[unfolded abbreviated_type_defs] : |
| "kinding [] (TFun (TPrim (Num U16)) (TPrim (Num U32))) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_4_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_5_script : tac list = [ |
| (RTac @{thm kind_tprim[where k = "{E,S,D}"]}) |
| ] *} |
| |
| |
| lemma typing_helper_5[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim (Num U64)) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_5_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_6_script : tac list = [ |
| (RTac @{thm kind_tfun[where k = "{E,S,D}"]}), |
| (RTac @{thm typing_helper_3}), |
| (RTac @{thm typing_helper_5}) |
| ] *} |
| |
| |
| lemma typing_helper_6[unfolded abbreviated_type_defs] : |
| "kinding [] (TFun (TPrim (Num U32)) (TPrim (Num U64))) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_6_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_7_script : tac list = [ |
| (RTac @{thm kind_tprod[where k = "{E,S,D}"]}), |
| (RTac @{thm typing_helper_3}), |
| (RTac @{thm typing_helper_3}) |
| ] *} |
| |
| |
| lemma typing_helper_7[unfolded abbreviated_type_defs] : |
| "kinding [] (TProduct (TPrim (Num U32)) (TPrim (Num U32))) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_7_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_8_script : tac list = [ |
| (RTac @{thm kind_tprim[where k = "{E,S,D}"]}) |
| ] *} |
| |
| |
| lemma typing_helper_8[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim Bool) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_8_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_9_script : tac list = [ |
| (RTac @{thm kind_tfun[where k = "{E,S,D}"]}), |
| (RTac @{thm typing_helper_3}), |
| (RTac @{thm typing_helper_1}) |
| ] *} |
| |
| |
| lemma typing_helper_9[unfolded abbreviated_type_defs] : |
| "kinding [] (TFun (TPrim (Num U32)) (TPrim (Num U16))) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_9_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_10_script : tac list = [ |
| (RTac @{thm kind_tprim[where k = "{E,S,D}"]}) |
| ] *} |
| |
| |
| lemma typing_helper_10[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim (Num U8)) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_10_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_11_script : tac list = [ |
| (RTac @{thm kind_tfun[where k = "{E,S,D}"]}), |
| (RTac @{thm typing_helper_10}), |
| (RTac @{thm typing_helper_3}) |
| ] *} |
| |
| |
| lemma typing_helper_11[unfolded abbreviated_type_defs] : |
| "kinding [] (TFun (TPrim (Num U8)) (TPrim (Num U32))) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_11_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_12_script : tac list = [ |
| (RTac @{thm kind_tprod[where k = "{E,S,D}"]}), |
| (RTac @{thm typing_helper_5}), |
| (RTac @{thm typing_helper_5}) |
| ] *} |
| |
| |
| lemma typing_helper_12[unfolded abbreviated_type_defs] : |
| "kinding [] (TProduct (TPrim (Num U64)) (TPrim (Num U64))) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_12_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_13_script : tac list = [ |
| (RTac @{thm kind_tunit[where k = "{E,S,D}"]}) |
| ] *} |
| |
| |
| lemma typing_helper_13[unfolded abbreviated_type_defs] : |
| "kinding [] TUnit {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_13_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_14_script : tac list = [ |
| (RTac @{thm kind_tsum[where k = "{E,S,D}"]}), |
| (SimpTac ([],[])), |
| (SimpTac ([],[])), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_13}), |
| (RTac @{thm kind_all_empty}) |
| ] *} |
| |
| |
| lemma typing_helper_14[unfolded abbreviated_type_defs] : |
| "kinding [] (TSum [(''Error'', TUnit)]) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_14_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_15_script : tac list = [ |
| (RTac @{thm kind_tsum[where k = "{E,S,D}"]}), |
| (SimpTac ([],[])), |
| (SimpTac ([],[])), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_3}), |
| (RTac @{thm kind_all_empty}) |
| ] *} |
| |
| |
| lemma typing_helper_15[unfolded abbreviated_type_defs] : |
| "kinding [] (TSum [(''Success'', TPrim (Num U32))]) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_15_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_16_script : tac list = [ |
| (RTac @{thm kind_tsum[where k = "{E,S,D}"]}), |
| (SimpTac ([],[])), |
| (SimpTac ([],[])), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_5}), |
| (RTac @{thm kind_all_empty}) |
| ] *} |
| |
| |
| lemma typing_helper_16[unfolded abbreviated_type_defs] : |
| "kinding [] (TSum [(''Success'', TPrim (Num U64))]) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_16_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_17_script : tac list = [ |
| (RTac @{thm kind_tcon[where k = "{E}"]}), |
| (RTac @{thm kind_all_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_17[unfolded abbreviated_type_defs] : |
| "kinding [] (TCon ''SysState'' [] Writable) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_17_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_18_script : tac list = [ |
| (RTac @{thm kind_tprim}) |
| ] *} |
| |
| |
| lemma typing_helper_18[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim (Num U32)) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_18_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_19_script : tac list = [ |
| (RTac @{thm kind_tprod[where k = "{E}"]}), |
| (RTac @{thm typing_helper_17}), |
| (RTac @{thm typing_helper_18}) |
| ] *} |
| |
| |
| lemma typing_helper_19[unfolded abbreviated_type_defs] : |
| "kinding [] (TProduct (TCon ''SysState'' [] Writable) (TPrim (Num U32))) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_19_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_20_script : tac list = [ |
| (RTac @{thm kind_tcon}), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_18}), |
| (RTac @{thm kind_all_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_20[unfolded abbreviated_type_defs] : |
| "kinding [] (TCon ''WordArray'' [TPrim (Num U32)] Writable) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_20_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_21_script : tac list = [ |
| (RTac @{thm kind_tprod}), |
| (RTac @{thm typing_helper_17}), |
| (RTac @{thm typing_helper_20}) |
| ] *} |
| |
| |
| lemma typing_helper_21[unfolded abbreviated_type_defs] : |
| "kinding [] (TProduct (TCon ''SysState'' [] Writable) (TCon ''WordArray'' [TPrim (Num U32)] Writable)) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_21_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_22_script : tac list = [ |
| (RTac @{thm kind_tsum[where k = "{E}"]}), |
| (SimpTac ([],[])), |
| (SimpTac ([],[])), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_17}), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_21}), |
| (RTac @{thm kind_all_empty}) |
| ] *} |
| |
| |
| lemma typing_helper_22[unfolded abbreviated_type_defs] : |
| "kinding [] (TSum [(''Error'', TCon ''SysState'' [] Writable), (''Success'', TProduct (TCon ''SysState'' [] Writable) (TCon ''WordArray'' [TPrim (Num U32)] Writable))]) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_22_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_23_script : tac list = [ |
| (RTac @{thm kind_tfun[where k = "{E,S,D}"]}), |
| (RTac @{thm typing_helper_19}), |
| (RTac @{thm typing_helper_22}) |
| ] *} |
| |
| |
| lemma typing_helper_23[unfolded abbreviated_type_defs] : |
| "kinding [] (TFun (TProduct (TCon ''SysState'' [] Writable) (TPrim (Num U32))) (TSum [(''Error'', TCon ''SysState'' [] Writable), (''Success'', TProduct (TCon ''SysState'' [] Writable) (TCon ''WordArray'' [TPrim (Num U32)] Writable))])) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_23_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_24_script : tac list = [ |
| (RTac @{thm kind_trec[where k = "{E}"]}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_20}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_18}), |
| (RTac @{thm kind_record_cons1}), |
| (RTac @{thm typing_helper_18}), |
| (RTac @{thm kind_record_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_24[unfolded abbreviated_type_defs] : |
| "kinding [] (TRecord [(TCon ''WordArray'' [TPrim (Num U32)] Writable, False), (TPrim (Num U32), False), (TPrim (Num U32), False)] Unboxed) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_24_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_25_script : tac list = [ |
| (RTac @{thm kind_tsum[where k = "{E}"]}), |
| (SimpTac ([],[])), |
| (SimpTac ([],[])), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_20}), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_20}), |
| (RTac @{thm kind_all_empty}) |
| ] *} |
| |
| |
| lemma typing_helper_25[unfolded abbreviated_type_defs] : |
| "kinding [] (TSum [(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable), (''Success'', TCon ''WordArray'' [TPrim (Num U32)] Writable)]) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_25_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_26_script : tac list = [ |
| (RTac @{thm kind_tfun[where k = "{E,S,D}"]}), |
| (RTac @{thm typing_helper_24}), |
| (RTac @{thm typing_helper_25}) |
| ] *} |
| |
| |
| lemma typing_helper_26[unfolded abbreviated_type_defs] : |
| "kinding [] (TFun (TRecord [(TCon ''WordArray'' [TPrim (Num U32)] Writable, False), (TPrim (Num U32), False), (TPrim (Num U32), False)] Unboxed) (TSum [(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable), (''Success'', TCon ''WordArray'' [TPrim (Num U32)] Writable)])) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_26_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_27_script : tac list = [ |
| (RTac @{thm kind_tprim}) |
| ] *} |
| |
| |
| lemma typing_helper_27[unfolded abbreviated_type_defs] : |
| "kinding [] (TPrim (Num U32)) {S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_27_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_28_script : tac list = [ |
| (RTac @{thm kind_tcon[where k = "{S,D}"]}), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_27}), |
| (RTac @{thm kind_all_empty}), |
| (SimpTac ([],[])) |
| ] *} |
| |
| |
| lemma typing_helper_28[unfolded abbreviated_type_defs] : |
| "kinding [] (TCon ''WordArray'' [TPrim (Num U32)] ReadOnly) {S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_28_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_29_script : tac list = [ |
| (RTac @{thm kind_tprod[where k = "{S,D}"]}), |
| (RTac @{thm typing_helper_28}), |
| (RTac @{thm typing_helper_27}) |
| ] *} |
| |
| |
| lemma typing_helper_29[unfolded abbreviated_type_defs] : |
| "kinding [] (TProduct (TCon ''WordArray'' [TPrim (Num U32)] ReadOnly) (TPrim (Num U32))) {S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_29_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_30_script : tac list = [ |
| (RTac @{thm kind_tfun[where k = "{E,S,D}"]}), |
| (RTac @{thm typing_helper_29}), |
| (RTac @{thm typing_helper_3}) |
| ] *} |
| |
| |
| lemma typing_helper_30[unfolded abbreviated_type_defs] : |
| "kinding [] (TFun (TProduct (TCon ''WordArray'' [TPrim (Num U32)] ReadOnly) (TPrim (Num U32))) (TPrim (Num U32))) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_30_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_31_script : tac list = [ |
| (RTac @{thm kind_tfun[where k = "{E,S,D}"]}), |
| (RTac @{thm typing_helper_21}), |
| (RTac @{thm typing_helper_17}) |
| ] *} |
| |
| |
| lemma typing_helper_31[unfolded abbreviated_type_defs] : |
| "kinding [] (TFun (TProduct (TCon ''SysState'' [] Writable) (TCon ''WordArray'' [TPrim (Num U32)] Writable)) (TCon ''SysState'' [] Writable)) {E, S, D}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_31_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_32_script : tac list = [ |
| (RTac @{thm kind_tsum[where k = "{E}"]}), |
| (SimpTac ([],[])), |
| (SimpTac ([],[])), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_20}), |
| (RTac @{thm kind_all_empty}) |
| ] *} |
| |
| |
| lemma typing_helper_32[unfolded abbreviated_type_defs] : |
| "kinding [] (TSum [(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable)]) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_32_script |> EVERY *}) |
| done |
| |
| ML {* |
| val typing_helper_33_script : tac list = [ |
| (RTac @{thm kind_tsum[where k = "{E}"]}), |
| (SimpTac ([],[])), |
| (SimpTac ([],[])), |
| (RTac @{thm kind_all_cons}), |
| (RTac @{thm typing_helper_17}), |
| (RTac @{thm kind_all_empty}) |
| ] *} |
| |
| |
| lemma typing_helper_33[unfolded abbreviated_type_defs] : |
| "kinding [] (TSum [(''Error'', TCon ''SysState'' [] Writable)]) {E}" |
| apply (unfold abbreviated_type_defs)? |
| apply (tactic {* map (fn t => DETERM (interpret_tac t @{context} 1)) typing_helper_33_script |> EVERY *}) |
| done |
| |
| ML {* |
| val u16_to_u64_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_1})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_1})], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (2,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_1})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm u16_to_u32_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_4}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm u32_to_u64_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_6}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma u16_to_u64_typecorrect : |
| "\<Xi>, fst u16_to_u64_type, (u16_to_u64_typetree, [Some (fst (snd u16_to_u64_type))]) T\<turnstile> u16_to_u64 : snd (snd u16_to_u64_type)" |
| apply (simp add: u16_to_u64_type_def u16_to_u64_def u16_to_u64_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm u16_to_u64_def} @{thm u16_to_u64_typetree_def} @{context} u16_to_u64_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| ML {* |
| val min_u32_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_7})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_7}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "3"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma min_u32_typecorrect : |
| "\<Xi>, fst min_u32_type, (min_u32_typetree, [Some (fst (snd min_u32_type))]) T\<turnstile> min_u32 : snd (snd min_u32_type)" |
| apply (simp add: min_u32_type_def min_u32_def min_u32_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm min_u32_def} @{thm min_u32_typetree_def} @{context} min_u32_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| ML {* |
| val cogent_low_16_bits_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_1})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_1}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})]),(2,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "4"]}),(SimpTac ([@{thm empty_def}],[]))], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (5,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm u32_to_u16_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_9}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma cogent_low_16_bits_typecorrect : |
| "\<Xi>, fst cogent_low_16_bits_type, (cogent_low_16_bits_typetree, [Some (fst (snd cogent_low_16_bits_type))]) T\<turnstile> cogent_low_16_bits : snd (snd cogent_low_16_bits_type)" |
| apply (simp add: cogent_low_16_bits_type_def cogent_low_16_bits_def cogent_low_16_bits_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm cogent_low_16_bits_def} @{thm cogent_low_16_bits_typetree_def} @{context} cogent_low_16_bits_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| ML {* |
| val cogent_high_16_bits_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "3"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_10})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (5,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_10})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm u8_to_u32_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_11}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_10}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (6,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})]),(2,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (6,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "6"]}),(SimpTac ([@{thm empty_def}],[]))], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (7,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm u32_to_u16_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_9}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma cogent_high_16_bits_typecorrect : |
| "\<Xi>, fst cogent_high_16_bits_type, (cogent_high_16_bits_typetree, [Some (fst (snd cogent_high_16_bits_type))]) T\<turnstile> cogent_high_16_bits : snd (snd cogent_high_16_bits_type)" |
| apply (simp add: cogent_high_16_bits_type_def cogent_high_16_bits_def cogent_high_16_bits_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm cogent_high_16_bits_def} @{thm cogent_high_16_bits_typetree_def} @{context} cogent_high_16_bits_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| ML {* |
| val align64_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_12})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_12}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "3"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_10})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_10}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (6,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_5})]),(2,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (6,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "6"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (7,[(4,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})]),(5,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (7,[(5,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "7"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (8,[(5,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})]),(6,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (8,[(6,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "8"]}),(SimpTac ([@{thm empty_def}],[]))], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (9,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_5})]),(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (9,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "9"]}),(SimpTac ([@{thm empty_def}],[]))], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma align64_typecorrect : |
| "\<Xi>, fst align64_type, (align64_typetree, [Some (fst (snd align64_type))]) T\<turnstile> align64 : snd (snd align64_type)" |
| apply (simp add: align64_type_def align64_def align64_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm align64_def} @{thm align64_typetree_def} @{context} align64_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| ML {* |
| val align32_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_7})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_7}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "3"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_10})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_10}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (6,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})]),(2,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (6,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "6"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (7,[(4,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(5,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (7,[(5,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "7"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (8,[(5,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(6,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (8,[(6,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "8"]}),(SimpTac ([@{thm empty_def}],[]))], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (9,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (9,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "9"]}),(SimpTac ([@{thm empty_def}],[]))], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma align32_typecorrect : |
| "\<Xi>, fst align32_type, (align32_typetree, [Some (fst (snd align32_type))]) T\<turnstile> align32 : snd (snd align32_type)" |
| apply (simp add: align32_type_def align32_def align32_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm align32_def} @{thm align32_typetree_def} @{context} align32_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| ML {* |
| val safe_add32_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_7})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_7}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "3"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (4,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "4"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (5,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(3,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (5,[(3,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "5"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (6,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_8})]),(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_8})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (6,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_8})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "6"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_unit}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}])], |
| KindingTacs [(RTac @{thm typing_helper_13})], |
| TypingTacs [(RTac @{thm typing_con}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_13}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_prom}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_14}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_3}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_con}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_3}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_prom}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_15}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_3}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma safe_add32_typecorrect : |
| "\<Xi>, fst safe_add32_type, (safe_add32_typetree, [Some (fst (snd safe_add32_type))]) T\<turnstile> safe_add32 : snd (snd safe_add32_type)" |
| apply (simp add: safe_add32_type_def safe_add32_def safe_add32_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm safe_add32_def} @{thm safe_add32_typetree_def} @{context} safe_add32_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| ML {* |
| val safe_add64_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_12})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_12}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "3"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (4,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "4"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (5,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})]),(3,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (5,[(3,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "5"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (6,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_8})]),(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_8})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (6,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_8})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "6"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_unit}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}])], |
| KindingTacs [(RTac @{thm typing_helper_13})], |
| TypingTacs [(RTac @{thm typing_con}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_13}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_prom}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_14}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_5}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_con}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_5}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_prom}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_16}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_5}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma safe_add64_typecorrect : |
| "\<Xi>, fst safe_add64_type, (safe_add64_typetree, [Some (fst (snd safe_add64_type))]) T\<turnstile> safe_add64 : snd (snd safe_add64_type)" |
| apply (simp add: safe_add64_type_def safe_add64_def safe_add64_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm safe_add64_def} @{thm safe_add64_typetree_def} @{context} safe_add64_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| ML {* |
| val safe_sub32_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_7})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_7}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "3"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (4,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "4"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_unit}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}])], |
| KindingTacs [(RTac @{thm typing_helper_13})], |
| TypingTacs [(RTac @{thm typing_con}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_13}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_prom}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_14}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_3}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| TypingTacs [(RTac @{thm typing_con}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_3}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_prom}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_15}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_3}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma safe_sub32_typecorrect : |
| "\<Xi>, fst safe_sub32_type, (safe_sub32_typetree, [Some (fst (snd safe_sub32_type))]) T\<turnstile> safe_sub32 : snd (snd safe_sub32_type)" |
| apply (simp add: safe_sub32_type_def safe_sub32_def safe_sub32_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm safe_sub32_def} @{thm safe_sub32_typetree_def} @{context} safe_sub32_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| ML {* |
| val safe_sub64_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_12})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_12}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (3,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "3"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_prim'}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (4,[(1,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_5})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "4"]}),(SimpTac ([@{thm empty_def}],[]))], |
| KindingTacs [(RTac @{thm typing_helper_8})], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_8}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_unit}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}])], |
| KindingTacs [(RTac @{thm typing_helper_13})], |
| TypingTacs [(RTac @{thm typing_con}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_13}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_prom}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_14}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_5}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_5})], |
| TypingTacs [(RTac @{thm typing_con}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_5}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_5}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_prom}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_16}]),(SimpTac ([],[])),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_13}),(RTac @{thm kind_all_cons}),(RTac @{thm typing_helper_5}),(RTac @{thm kind_all_empty}),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma safe_sub64_typecorrect : |
| "\<Xi>, fst safe_sub64_type, (safe_sub64_typetree, [Some (fst (snd safe_sub64_type))]) T\<turnstile> safe_sub64 : snd (snd safe_sub64_type)" |
| apply (simp add: safe_sub64_type_def safe_sub64_def safe_sub64_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm safe_sub64_def} @{thm safe_sub64_typetree_def} @{context} safe_sub64_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| ML {* |
| val caller_typecorrect_script : hints list = [ |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_17}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_10})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_10}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| TypingTacs [(RTac @{thm typing_tuple}),(SplitsTac (4,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})]),(2,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_17})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_17}]),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_19})], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (5,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_19})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm wordarray_create_0_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_23}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_19}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_22})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_22}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_21})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_21}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| KindingTacs [(RTac @{thm typing_helper_20})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_10})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| KindingTacs [(RTac @{thm typing_helper_20})], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (10,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_10})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm u8_to_u32_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_11}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_10}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| KindingTacs [(RTac @{thm typing_helper_20})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_10})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| KindingTacs [(RTac @{thm typing_helper_20})], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (12,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_10})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm u8_to_u32_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_11}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_10}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| KindingTacs [(RTac @{thm typing_helper_20})], |
| TypingTacs [(RTac @{thm typing_struct'}),(RTac @{thm typing_all_cons}),(SplitsTac (13,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})]),(2,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})]),(5,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_20})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_20}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (13,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})]),(2,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_cons}),(SplitsTac (13,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[])),(RTac @{thm typing_all_empty'[where n = "13"]}),(SimpTac ([@{thm empty_def}],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_24})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (14,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_24})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm wordarray_put_0_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_26}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_24}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_25})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_25}]),(SimpTac ([],[]))], |
| TTSplitBangTacs [(RTac @{thm ttsplit_bangI}),(SimpTac ([],[])),(SimpTac ([],[])),(ForceTac []),(RTac @{thm ttsplit_bang_innerI(5)}),(RTac @{thm typing_helper_20}),(SimpTac ([],[])),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(2)}),(RTac @{thm typing_helper_17}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(1)}),(RTac @{thm ttsplit_bang_innerI(6)})], |
| KindingTacs [(RTac @{thm typing_helper_28})], |
| TypingTacs [(RTac @{thm typing_lit'}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_10})], |
| KindingTacs [(RTac @{thm typing_helper_28})], |
| TypingTacs [(RTac @{thm typing_cast}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_10}]),(SimpTac ([],[])),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_28})], |
| TypingTacs [(RTac @{thm typing_tuple}),(SplitsTac (18,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_3})]),(2,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_28})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_28}]),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3}]),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (19,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_29})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm wordarray_get_0_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_30}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_29}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_20})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| TypingTacs [(RTac @{thm typing_tuple}),(SplitsTac (17,[(0,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_3})]),(1,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_20})]),(8,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_17})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_3},@{thm typing_helper_17}]),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_20}]),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (18,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_21})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm wordarray_free_0_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_31}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_21}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_3})], |
| KindingTacs [(RTac @{thm typing_helper_32})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| TypingTacs [(RTac @{thm typing_esac}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_32}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_20})], |
| KindingTacs [(RTac @{thm typing_helper_17})], |
| TypingTacs [(RTac @{thm typing_tuple}),(SplitsTac (17,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_20})]),(8,[(RTac @{thm split_comp.left}),(RTac @{thm typing_helper_17})])])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_17}]),(SimpTac ([],[])),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_20}]),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_app}),(SplitsTac (18,[(0,[(RTac @{thm split_comp.right}),(RTac @{thm typing_helper_21})])])),(RTac @{thm typing_afun'}),(SimpTac ([@{thm \<Xi>_def},@{thm wordarray_free_0_type_def[unfolded abbreviated_type_defs]}],[])),(RTac @{thm typing_helper_2}),(SimpTac ([],[])),(SimpTac ([],[])),(RTac @{thm exI[where x = "{E,S,D}"]}),(RTac @{thm typing_helper_31}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac []),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_21}]),(SimpTac ([],[]))], |
| KindingTacs [(RTac @{thm typing_helper_33})], |
| TypingTacs [(RTac @{thm typing_esac}),(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_33}]),(SimpTac ([],[]))], |
| TypingTacs [(RTac @{thm typing_var}),(SimpTac ([@{thm empty_def}],[])),(WeakeningTac [@{thm typing_helper_17}]),(SimpTac ([],[]))] |
| ] *} |
| |
| |
| lemma caller_typecorrect : |
| "\<Xi>, fst caller_type, (caller_typetree, [Some (fst (snd caller_type))]) T\<turnstile> caller : snd (snd caller_type)" |
| apply (simp add: caller_type_def caller_def caller_typetree_def replicate_unfold abbreviated_type_defs) |
| apply (tactic {* mk_ttsplit_tacs @{thm caller_def} @{thm caller_typetree_def} @{context} caller_typecorrect_script |
| |> map (fn t => DETERM (interpret_tac t @{context} 1)) |> EVERY *}) |
| done |
| |
| |
| (* Manual specification for abstract functions *) |
| definition |
| "u8_to_u32 \<sigma>x \<sigma>x'= (case \<sigma>x of (\<sigma>, UPrim (LU8 x)) \<Rightarrow> \<sigma>x' = (\<sigma>, UPrim (LU32 (ucast x))))" |
| |
| definition |
| "wordarray_get_0 args ret \<equiv> case args of |
| (\<sigma>, UProduct (UPtr wa_ptr _) (UPrim (LU32 i))) \<Rightarrow> |
| case \<sigma> wa_ptr of |
| Some (UAbstract (Abstyp_WordArray_U32 (vals, ptr))) \<Rightarrow> |
| ret = (\<sigma>, UPrim (LU32 (if unat i < length vals then vals ! unat i else 0)))" |
| |
| definition |
| "wordarray_put_0 args ret \<equiv> case args of |
| (\<sigma>, URecord [(UPtr wa_ptr wa_ptr_repr, _), |
| (UPrim (LU32 i), _), |
| (UPrim (LU32 val), _)]) \<Rightarrow> |
| case \<sigma> wa_ptr of |
| Some (UAbstract (Abstyp_WordArray_U32 (vals, ptr))) \<Rightarrow> |
| ret = |
| (if unat i < length vals |
| then (\<sigma>(wa_ptr := Some (UAbstract (Abstyp_WordArray_U32 (vals[unat i := val], ptr)))), |
| USum ''Success'' (UPtr wa_ptr wa_ptr_repr) [(''Success'', wa_ptr_repr)]) |
| else (\<sigma>, USum ''Error'' (UPtr wa_ptr wa_ptr_repr) [(''Error'', wa_ptr_repr)]))" |
| |
| definition |
| "\<xi> func_name \<equiv> case func_name of |
| ''cogent_log2'' \<Rightarrow> undefined |
| | ''random_u32'' \<Rightarrow> undefined |
| | ''test_file_close'' \<Rightarrow> undefined |
| | ''test_file_open'' \<Rightarrow> undefined |
| | ''test_file_read_next_u32'' \<Rightarrow> undefined |
| | ''test_stack_probe'' \<Rightarrow> undefined |
| | ''test_time_end'' \<Rightarrow> undefined |
| | ''test_time_start'' \<Rightarrow> undefined |
| | ''u16_to_u32'' \<Rightarrow> undefined |
| | ''u16_to_u8'' \<Rightarrow> undefined |
| | ''u32_to_u16'' \<Rightarrow> undefined |
| | ''u32_to_u64'' \<Rightarrow> undefined |
| | ''u32_to_u8'' \<Rightarrow> undefined |
| | ''u64_to_u32'' \<Rightarrow> undefined |
| | ''u8_to_u16'' \<Rightarrow> undefined |
| | ''u8_to_u32'' \<Rightarrow> u8_to_u32 |
| | ''u8_to_u64'' \<Rightarrow> undefined |
| | ''wordarray_cmp'' \<Rightarrow> undefined |
| | ''wordarray_create_0'' \<Rightarrow> undefined |
| | ''wordarray_free_0'' \<Rightarrow> undefined |
| | ''wordarray_get_0'' \<Rightarrow> wordarray_get_0 |
| | ''wordarray_put_0'' \<Rightarrow> wordarray_put_0" |
| |
| ML {* |
| val caller_typing_bucket = |
| mk_ttsplit_tacs_final @{thm caller_def} @{thm caller_typetree_def} @{context} caller_typecorrect_script |
| |> map (fn t => fn ctxt => t ctxt 1) |
| |> get_typing_bucket @{context} "caller" |
| *} |
| |
| new_C_include_dir "stdlib" |
| new_C_include_dir "../../cogent/tests/antiquote-tests/test-wordarray" |
| new_C_include_dir "../../cogent/tests/antiquote-tests/plat/console" |
| |
| install_C_file "wordarraytest.c" |
| autocorres [no_opt, ts_rules=nondet] "wordarraytest.c" |
| |
| (* C type and value relations *) |
| instantiation unit_t_C :: cogent_C_val begin |
| definition type_rel_unit_t_C_def: "type_rel r (_ :: unit_t_C itself) \<equiv> r = RUnit" |
| definition val_rel_unit_t_C_def: "val_rel uv (_ :: unit_t_C) \<equiv> uv = UUnit" |
| instance .. |
| end |
| |
| instantiation WordArray_u8_C :: cogent_C_val begin |
| definition type_rel_WordArray_u8_C_def: |
| "type_rel r (_ :: WordArray_u8_C itself) \<equiv> r = RCon ''WordArray'' [RPrim (Num U8)]" |
| definition val_rel_WordArray_u8_C_def: |
| "val_rel uv (arr :: WordArray_u8_C) \<equiv> |
| \<exists>vals ptr. uv = UAbstract (Abstyp_WordArray_U8 (vals, Ptr ptr)) \<and> |
| val_rel (UPtr ptr (RPtr (RPrim (Num U8)))) (WordArray_u8_C.values_C arr)" |
| instance .. |
| end |
| |
| instantiation WordArray_u32_C :: cogent_C_val begin |
| definition type_rel_WordArray_u32_C_def: |
| "type_rel r (_ :: WordArray_u32_C itself) \<equiv> r = RCon ''WordArray'' [RPrim (Num U32)]" |
| definition val_rel_WordArray_u32_C_def: |
| "val_rel uv (arr :: WordArray_u32_C) \<equiv> |
| \<exists>vals ptr. uv = UAbstract (Abstyp_WordArray_U32 (vals, Ptr ptr)) \<and> |
| val_rel (UPtr ptr (RPtr (RPrim (Num U32)))) (WordArray_u32_C.values_C arr)" |
| instance .. |
| end |
| |
| instantiation SysState_t_C :: cogent_C_val begin |
| definition type_rel_SysState_t_C_def: |
| "type_rel r (_ :: SysState_t_C itself) \<equiv> r = RCon ''SysState'' []" |
| definition val_rel_SysState_t_C_def: |
| "val_rel uv (_ :: SysState_t_C) \<equiv> uv = UAbstract Abstyp_SysState" |
| instance .. |
| end |
| |
| local_setup {* fn lthy => local_setup_val_rel_type_rel "wordarraytest.c" lthy *} |
| find_theorems name:val_rel_ -name:word |
| lemmas val_rel_simps = |
| val_rel_word val_rel_ptr_def val_rel_unit_def val_rel_unit_t_C_def |
| val_rel_t1_C_def val_rel_t2_C_def val_rel_t3_C_def val_rel_t4_C_def |
| val_rel_t5_C_def val_rel_t6_C_def val_rel_t7_C_def val_rel_t8_C_def |
| val_rel_t9_C_def val_rel_t10_C_def val_rel_t11_C_def val_rel_t12_C_def |
| val_rel_t13_C_def val_rel_t18_C_def val_rel_t40_C_def val_rel_t61_C_def |
| val_rel_t64_C_def val_rel_t67_C_def val_rel_t75_C_def val_rel_t80_C_def |
| val_rel_t119_C_def val_rel_t123_C_def val_rel_WordArray_u8_C_def val_rel_WordArray_u32_C_def |
| |
| class cogent_C_heap = cogent_C_val + |
| fixes is_valid :: "lifted_globals \<Rightarrow> 'a ptr \<Rightarrow> bool" |
| fixes heap :: "lifted_globals \<Rightarrow> 'a ptr \<Rightarrow> 'a" |
| fixes heap_update :: "(('a ptr \<Rightarrow> 'a) \<Rightarrow> 'a ptr \<Rightarrow> 'a) \<Rightarrow> lifted_globals \<Rightarrow> lifted_globals" |
| |
| instantiation WordArray_u8_C :: cogent_C_heap |
| begin |
| definition is_valid_WordArray_u8_C_def: "is_valid \<equiv> is_valid_WordArray_u8_C" |
| definition heap_WordArray_u8_C_def: "heap \<equiv> heap_WordArray_u8_C" |
| definition heap_WordArray_u8_C_update_def: "heap_update \<equiv> heap_WordArray_u8_C_update" |
| instance .. |
| end |
| |
| instantiation WordArray_u32_C :: cogent_C_heap |
| begin |
| definition is_valid_WordArray_u32_C_def: "is_valid \<equiv> is_valid_WordArray_u32_C" |
| definition heap_WordArray_u32_C_def: "heap \<equiv> heap_WordArray_u32_C" |
| definition heap_WordArray_u32_C_update_def: "heap_update \<equiv> heap_WordArray_u32_C_update" |
| instance .. |
| end |
| |
| axiomatization where wordarray_create_0_corres: |
| "val_rel x x' \<Longrightarrow> |
| update_sem_init.corres abs_typing abs_repr srel (App (AFun ''wordarray_create_0'' []) (Var 0)) |
| (do retval \<leftarrow> wordarraytest.wordarray_create_0' x'; gets (\<lambda>_. retval) od) |
| \<xi> (x # \<gamma>) \<Xi> (Some t # \<Gamma>') \<sigma> s" |
| |
| axiomatization where wordarray_free_0_corres: |
| "val_rel x x' \<Longrightarrow> |
| update_sem_init.corres abs_typing abs_repr srel (App (AFun ''wordarray_free_0'' []) (Var 0)) |
| (do retval \<leftarrow> wordarraytest.wordarray_free_0' x'; gets (\<lambda>_. retval) od) |
| \<xi> (x # \<gamma>) \<Xi> (Some t # \<Gamma>') \<sigma> s" |
| |
| locale WordArrayTest = wordarraytest begin |
| definition "abs_repr' a \<equiv> case a of |
| Abstyp_WordArray_U8 _ \<Rightarrow> (''WordArray'', [RPrim (Num U8)]) |
| | Abstyp_WordArray_U32 _ \<Rightarrow> (''WordArray'', [RPrim (Num U32)]) |
| | Abstyp_SysState \<Rightarrow> (''SysState'', [])" |
| |
| definition "abs_typing' a name \<tau>s sig (r :: ptrtyp set) (w :: ptrtyp set) \<equiv> |
| r = {} \<and> w = {} \<and> sig \<noteq> Unboxed \<and> |
| (case a of |
| Abstyp_WordArray_U8 _ \<Rightarrow> name = ''WordArray'' \<and> \<tau>s = [TPrim (Num U8)] |
| | Abstyp_WordArray_U32 _ \<Rightarrow> name = ''WordArray'' \<and> \<tau>s = [TPrim (Num U32)] |
| | Abstyp_SysState \<Rightarrow> name = ''SysState'' \<and> \<tau>s = [])" |
| end |
| |
| sublocale WordArrayTest \<subseteq> |
| update_sem_init abs_typing' abs_repr' |
| apply (unfold abs_repr'_def[abs_def] abs_typing'_def[abs_def]) |
| apply unfold_locales |
| |
| apply (clarsimp split: abstyp.splits) |
| apply (case_tac s, simp_all)[] |
| apply (case_tac s, simp_all)[] |
| apply (case_tac s, simp_all)[] |
| |
| apply simp |
| |
| apply simp |
| |
| apply simp |
| |
| apply simp |
| |
| apply (clarsimp split: abstyp.splits) |
| apply (case_tac s, (case_tac s', simp_all)+)[] |
| apply (case_tac s, (case_tac s', simp_all)+)[] |
| apply (case_tac s, (case_tac s', simp_all)+)[] |
| |
| apply (clarsimp split: abstyp.splits) |
| done |
| |
| (* FIXME: syntax translations from UpdateSemantics are not available in WordArrayTest‽ *) |
| context WordArrayTest begin |
| |
| thm wordarray_create_0'_def |
| thm wordarray_free_0'_def |
| thm wordarray_put_0'_def |
| thm wordarray_get_0'_def |
| thm caller_def caller'_def |
| |
| lemma return_exn_simp: |
| "do ret <- A; |
| _ <- guard (\<lambda>_. True); |
| _ <- gets (\<lambda>_. x :: c_exntype); |
| _ <- guard (\<lambda>_. True); |
| _ <- gets (\<lambda>_. ()); |
| _ <- guard (\<lambda>_. True); |
| gets (\<lambda>_. ret) od = A" |
| by simp |
| |
| (* Relation between program heaps *) |
| definition |
| heap_rel_ptr :: |
| "(funtyp, abstyp, ptrtyp) store \<Rightarrow> lifted_globals \<Rightarrow> |
| ('a :: cogent_C_heap) ptr \<Rightarrow> bool" |
| where |
| "heap_rel_ptr \<sigma> h p \<equiv> |
| (\<forall>uv. |
| \<sigma> (ptr_val p) = Some uv \<longrightarrow> |
| type_rel (uval_repr uv) TYPE('a) \<longrightarrow> |
| is_valid h p \<and> val_rel uv (heap h p))" |
| |
| definition |
| "heap_rel_WordArray_u32_C \<sigma> h p \<equiv> |
| (\<forall>uv. |
| \<sigma> (ptr_val p) = Some uv \<longrightarrow> |
| type_rel (uval_repr uv) TYPE(WordArray_u32_C) \<longrightarrow> |
| (\<exists>vals ptr. uv = UAbstract (Abstyp_WordArray_U32 (vals, ptr)) \<and> |
| is_valid h p \<and> |
| val_rel (UAbstract (Abstyp_WordArray_U32 (vals, ptr))) (heap h p) \<and> |
| unat (WordArray_u32_C.len_C (heap h p)) = length vals \<and> |
| 0 <=s WordArray_u32_C.len_C (heap h p) \<and> |
| (\<forall>(i::word32) < ucast (WordArray_u32_C.len_C (heap h p)). |
| c_guard (WordArray_u32_C.values_C (heap h p) +\<^sub>p uint i) \<and> |
| is_valid_w32 h (WordArray_u32_C.values_C (heap h p) +\<^sub>p uint i) \<and> |
| heap_w32 h (WordArray_u32_C.values_C (heap h p) +\<^sub>p uint i) = vals ! unat i)))" |
| |
| definition heap_rel :: "(funtyp, abstyp, ptrtyp) store \<Rightarrow> lifted_globals \<Rightarrow> bool" |
| where |
| "heap_rel \<sigma> h \<equiv> |
| (\<forall>(p :: WordArray_u8_C ptr). heap_rel_ptr \<sigma> h p) \<and> (* TODO *) |
| (\<forall>(p :: WordArray_u32_C ptr). heap_rel_WordArray_u32_C \<sigma> h p)" |
| |
| definition state_rel :: "((funtyp, abstyp, ptrtyp) store \<times> lifted_globals) set" |
| where |
| "state_rel = {(\<sigma>, h). heap_rel \<sigma> h}" |
| |
| |
| (* To be proven *) |
| thm wordarray_put_0_def |
| lemma wordarray_put_0_corres: |
| "val_rel x x' \<Longrightarrow> |
| corres state_rel (App (AFun ''wordarray_put_0'' []) (Var 0)) |
| (do retval \<leftarrow> wordarray_put_0' x'; gets (\<lambda>_. retval) od) |
| \<xi> (x # \<gamma>) \<Xi> (Some (TRecord [(TCon ''WordArray'' [TPrim (Num U32)] Writable, False), (TPrim (Num U32), False), (TPrim (Num U32), False)] Unboxed) # \<Gamma>') \<sigma> s" |
| apply (rule corres_app_abstract) |
| apply (simp add: \<xi>_def) |
| apply (monad_eq simp: wordarray_put_0'_def) |
| apply (clarsimp simp add: state_rel_def heap_rel_def) |
| apply (erule_tac x="arr_C x'" in allE) |
| apply (clarsimp simp: heap_rel_WordArray_u32_C_def) |
| apply (clarsimp simp add: val_rel_simps type_rel_WordArray_u32_C_def) |
| apply (erule u_t_recE, simp) |
| apply (erule uval_typing_record.cases, simp_all) |
| apply (erule uval_typing.cases, simp_all) |
| apply (clarsimp simp: is_valid_WordArray_u32_C_def) |
| apply (erule impE) |
| apply (force dest: abs_typing_repr) |
| apply (clarsimp simp: is_valid_WordArray_u32_C_def) |
| apply (erule_tac x="scast (idx_C x')" in allE) |
| apply (simp add: heap_WordArray_u32_C_def) |
| apply (erule impE) |
| apply (simp add: word_not_le) |
| apply (subst (asm) scast_eq_ucast) |
| apply (simp add: word_msb_sint not_le[symmetric]) |
| apply (drule word_sle_def[THEN iffD1]) |
| apply simp |
| apply simp |
| apply simp |
| |
| apply (monad_eq simp: wordarray_put_0'_def wordarray_put_0_def val_rel_simps) |
| apply (clarsimp simp: state_rel_def) |
| apply (frule heap_rel_def[THEN meta_eq_to_obj_eq, THEN iffD1]) |
| apply clarsimp |
| apply (erule_tac x="arr_C x'" in allE) |
| apply (clarsimp simp: heap_rel_WordArray_u32_C_def heap_WordArray_u32_C_def) |
| apply (erule u_t_recE) |
| apply (erule uval_typing_record.cases, simp_all) |
| apply (erule uval_typing.cases, simp_all) |
| apply clarsimp |
| apply (frule abs_typing_repr) |
| apply (clarsimp simp: type_rel_WordArray_u32_C_def) |
| apply (case_tac "scast (WordArray_u32_C.len_C (heap_WordArray_u32_C s (arr_C x'))) \<le> idx_C x'") |
| |
| apply (clarsimp simp: TAG_ENUM_Success_def TAG_ENUM_Error_def) |
| apply (subst (asm) scast_eq_ucast) |
| apply (simp add: word_msb_sint not_le[symmetric]) |
| apply (drule word_sle_def[THEN iffD1]) |
| apply simp |
| apply (unat_arith) |
| apply (simp add: unat_ucast_upcast is_up) |
| |
| apply (clarsimp simp: heap_rel_def TAG_ENUM_Success_def TAG_ENUM_Error_def) |
| apply (rule exI)+ |
| apply (rule conjI) |
| |
| apply (clarsimp simp: heap_rel_ptr_def) |
| apply (rule conjI) |
| apply simp |
| apply simp |
| apply (erule uval_typing_record.cases, simp_all) |
| apply clarsimp |
| apply (erule uval_typing.cases, simp_all) |
| apply (erule uval_typing_record.cases, simp_all) |
| apply (erule uval_typing.cases, simp_all) |
| apply clarify |
| apply (subgoal_tac "(idx_C x') = val_C x'") |
| sorry |
| |
| |
| (* alternate proof attempt *) |
| lemma word32_small_shift_eq: |
| "\<lbrakk> 0 < k; k < 32; |
| (x :: word32) < 2^(32 - k); |
| y < 2^(32 - k); |
| x << k = y << k \<rbrakk> \<Longrightarrow> |
| x = y" |
| apply (rule word_unat.Rep_eqD) |
| apply (drule unat_cong) |
| apply (subst (asm) shiftl_t2n)+ |
| apply (subst (asm) unat_mult_simple) |
| apply (drule unat_mono) |
| apply (drule mult_less_mono2[where k = "unat (2 ^ k :: word32)" and i = "unat x"]) |
| apply (rule unat_1_0[THEN iffD1]) |
| apply (rule word_1_le_power) |
| apply simp |
| apply (subst (asm) unat_power_lower, simp)+ |
| apply (subst (asm) power_add[symmetric], simp) |
| apply (subst (asm) unat_mult_simple[where y = y]) |
| apply (drule unat_mono[where a = y]) |
| apply (drule mult_less_mono2[where k = "unat (2 ^ k :: word32)" and i = "unat y"]) |
| apply (rule unat_1_0[THEN iffD1]) |
| apply (rule word_1_le_power) |
| apply simp |
| apply (subst (asm) unat_power_lower, simp)+ |
| apply (subst (asm) power_add[symmetric], simp) |
| apply simp |
| done |
| |
| lemma ptr_aligned_plus2: |
| assumes aligned: "ptr_aligned (p +\<^sub>p i)" |
| shows "ptr_aligned (p::'a::mem_type ptr)" |
| proof - |
| have "int (align_of TYPE('a)) dvd (i * int (size_of TYPE('a)))" |
| by (metis dvd_mult zdvd_int align_size_of) |
| with aligned show ?thesis |
| apply (case_tac p, simp add: ptr_aligned_def ptr_add_def scast_id) |
| apply (simp only: unat_simps len_signed) |
| apply (drule dvd_mod_imp_dvd[OF _ align]) |
| apply (fastforce elim: dvd_plus_eq_left[THEN iffD1, rotated] |
| simp: dvd_mod[OF _ align] align_size_of) |
| done |
| qed |
| |
| lemma wordarray_put_0_corres: |
| "val_rel x x' \<Longrightarrow> |
| corres state_rel (App (AFun ''wordarray_put_0'' []) (Var 0)) |
| (do retval \<leftarrow> wordarray_put_0' x'; gets (\<lambda>_. retval) od) |
| \<xi> (x # \<gamma>) \<Xi> |
| (Some (TRecord |
| [(TCon ''WordArray'' [TPrim (Num U32)] Writable, False), |
| (TPrim (Num U32), False), (TPrim (Num U32), False)] Unboxed) # \<Gamma>') |
| \<sigma> s" |
| apply (rule corres_app_abstract) |
| apply (simp add: \<xi>_def) |
| apply (monad_eq simp: wordarray_put_0'_def) |
| apply (clarsimp simp add: state_rel_def heap_rel_def) |
| apply (erule_tac x="t3_C.arr_C x'" in allE) |
| apply (clarsimp simp: heap_rel_WordArray_u32_C_def) |
| apply (clarsimp simp add: val_rel_simps type_rel_WordArray_u32_C_def) |
| apply (erule uval_typing.cases uval_typing_record.cases, simp_all)+ |
| apply clarify |
| apply (thin_tac "Num U32 = lit_type (LU32 (t3_C.idx_C x'))") (* FIXME: simplifier loop *) |
| apply (thin_tac "Num U32 = lit_type (LU32 (t3_C.val_C x'))") |
| apply clarsimp |
| apply (erule impE) |
| apply (force dest: abs_typing_repr) |
| apply (clarsimp simp: is_valid_WordArray_u32_C_def) |
| apply (erule_tac x="scast (t3_C.idx_C x')" in allE) |
| apply (simp add: heap_WordArray_u32_C_def) |
| apply (erule impE) |
| apply (simp add: word_not_le) |
| apply (subst (asm) scast_eq_ucast) |
| apply (simp add: word_msb_sint not_le[symmetric]) |
| apply (drule word_sle_def[THEN iffD1]) |
| apply simp |
| apply simp |
| apply simp |
| |
| apply (monad_eq simp: wordarray_put_0'_def wordarray_put_0_def val_rel_simps) |
| apply (clarsimp simp: state_rel_def heap_rel_def) |
| apply (frule_tac x="t3_C.arr_C x'" in spec) |
| apply (clarsimp simp: heap_rel_WordArray_u32_C_def heap_WordArray_u32_C_def) |
| apply (erule uval_typing.cases uval_typing_record.cases, simp_all)+ |
| apply clarify |
| apply (thin_tac "Num U32 = lit_type (LU32 (t3_C.idx_C x'))") (* FIXME: simplifier loop *) |
| apply (thin_tac "Num U32 = lit_type (LU32 (t3_C.val_C x'))") |
| apply clarsimp |
| apply (drule abs_typing_repr) |
| apply (clarsimp simp: type_rel_WordArray_u32_C_def) |
| apply (subst (asm) scast_eq_ucast, |
| simp add: word_msb_sint not_le[symmetric], |
| drule word_sle_def[THEN iffD1], simp)+ |
| apply (subgoal_tac "unat (WordArray_u32_C.len_C (heap_WordArray_u32_C s (t3_C.arr_C x'))) |
| = unat (ucast (WordArray_u32_C.len_C (heap_WordArray_u32_C s (t3_C.arr_C x'))) :: word32)") |
| prefer 2 |
| apply (simp add: unat_ucast_upcast is_up) |
| apply clarsimp |
| apply (rule_tac x="if unat (idx_C x') < length vals |
| then \<sigma>(ptr_val (arr_C x') \<mapsto> |
| UAbstract (Abstyp_WordArray_U32 (vals[unat (idx_C x') := val_C x'], ptr))) |
| else \<sigma>" in exI) |
| apply (rule_tac x="if unat (idx_C x') < length vals |
| then USum ''Success'' (UPtr (ptr_val (arr_C x')) (RCon ''WordArray'' [RPrim (Num U32)])) |
| [(''Success'', RCon ''WordArray'' [RPrim (Num U32)])] |
| else USum ''Error'' (UPtr (ptr_val (arr_C x')) (RCon ''WordArray'' [RPrim (Num U32)])) |
| [(''Error'', RCon ''WordArray'' [RPrim (Num U32)])]" in exI) |
| apply clarsimp |
| apply (rule conjI) |
| (* The heap gets updated *) |
| apply (clarsimp simp: heap_rel_ptr_def[abs_def] abs_repr'_def) |
| apply (clarsimp simp: type_rel_WordArray_u8_C_def) |
| apply (rule conjI) |
| (* WordArray_U8 heap is unaffected *) |
| apply (fastforce simp: is_valid_WordArray_u8_C_def heap_WordArray_u8_C_def) |
| |
| (* WordArray_U32 heap update *) |
| apply (intro conjI impI allI) |
| apply (rename_tac p) |
| apply (clarsimp simp: heap_rel_WordArray_u32_C_def |
| heap_WordArray_u32_C_def is_valid_WordArray_u32_C_def) |
| apply (subgoal_tac "t3_C.idx_C x' < ucast (WordArray_u32_C.len_C (heap_WordArray_u32_C s (t3_C.arr_C x')))") |
| prefer 2 |
| apply (rule unat_less_impl_less) |
| apply (simp add: unat_ucast_upcast is_up) |
| apply clarsimp |
| apply (intro conjI impI) |
| apply (fastforce simp: val_rel_WordArray_u32_C_def val_rel_ptr_def) |
| apply (rule allI, rename_tac i) |
| apply (rule conjI) |
| apply clarsimp |
| apply (subgoal_tac "i = idx_C x'") |
| apply simp |
| apply (frule_tac x=i in spec) |
| apply (clarsimp simp: ptr_add_def c_guard_def) |
| apply (rule word32_small_shift_eq[where k = 2, simplified shiftl_t2n, simplified]) |
| apply (subst word_not_le[symmetric], clarsimp) |
| apply (clarsimp simp: c_null_guard_def) |
| defer (* i < 2^30 *) |
| defer |
| apply (metis mult.commute[where 'a = word32]) |
| apply clarsimp |
| apply (subgoal_tac "i \<noteq> idx_C x'") |
| apply simp |
| apply (clarsimp simp: ptr_add_def c_guard_def) |
| apply (drule_tac x=p in spec) |
| apply (clarsimp simp: heap_rel_WordArray_u32_C_def is_valid_WordArray_u32_C_def heap_WordArray_u32_C_def) |
| oops |
| |
| lemma wordarray_get_0_corres: |
| "val_rel x x' \<Longrightarrow> |
| corres state_rel (App (AFun ''wordarray_get_0'' []) (Var 0)) |
| (do retval \<leftarrow> wordarray_get_0' x'; gets (\<lambda>_. retval) od) |
| \<xi> (x # \<gamma>) \<Xi> (Some (TProduct (TCon ''WordArray'' [TPrim (Num U32)] ReadOnly) (TPrim (Num U32))) # \<Gamma>') \<sigma> s" |
| apply (rule corres_app_abstract) |
| apply (simp add: \<xi>_def) |
| apply (monad_eq simp: wordarray_get_0'_def) |
| apply (clarsimp simp add: state_rel_def heap_rel_def) |
| apply (erule_tac x="t2_C.p1_C x'" in allE) |
| apply (clarsimp simp: heap_rel_WordArray_u32_C_def) |
| apply (clarsimp simp add: val_rel_simps type_rel_WordArray_u32_C_def) |
| apply (erule u_t_productE, clarsimp) |
| apply (erule uval_typing.cases, simp_all) |
| apply (erule impE) |
| apply (force dest: abs_typing_repr) |
| apply (clarsimp simp: is_valid_WordArray_u32_C_def) |
| apply (erule_tac x="scast (t2_C.p2_C x')" in allE) |
| apply (simp add: heap_WordArray_u32_C_def) |
| apply (erule impE) |
| apply (simp add: word_not_le) |
| apply (subst (asm) scast_eq_ucast) |
| apply (simp add: word_msb_sint not_le[symmetric]) |
| apply (drule word_sle_def[THEN iffD1]) |
| apply simp |
| apply simp |
| apply simp |
| |
| apply (monad_eq simp: wordarray_get_0'_def wordarray_get_0_def val_rel_simps) |
| apply (clarsimp simp: state_rel_def) |
| apply (frule heap_rel_def[THEN meta_eq_to_obj_eq, THEN iffD1]) |
| apply clarsimp |
| apply (erule_tac x="t2_C.p1_C x'" in allE) |
| apply (clarsimp simp: heap_rel_WordArray_u32_C_def heap_WordArray_u32_C_def) |
| apply (erule u_t_productE) |
| apply (erule uval_typing.cases, simp_all) |
| apply clarsimp |
| apply (drule abs_typing_repr) |
| apply (clarsimp simp: type_rel_WordArray_u32_C_def) |
| apply (subgoal_tac "s' = s") |
| prefer 2 |
| apply (case_tac "scast (WordArray_u32_C.len_C (heap_WordArray_u32_C s (t2_C.p1_C x'))) \<le> t2_C.p2_C x'") |
| apply simp |
| apply simp |
| apply clarsimp |
| apply (subst (asm) scast_eq_ucast, |
| simp add: word_msb_sint not_le[symmetric], |
| drule word_sle_def[THEN iffD1], simp)+ |
| apply (subgoal_tac "unat (WordArray_u32_C.len_C (heap_WordArray_u32_C s (t2_C.p1_C x'))) |
| = unat (ucast (WordArray_u32_C.len_C (heap_WordArray_u32_C s (t2_C.p1_C x'))) :: word32)") |
| prefer 2 |
| apply (simp add: unat_ucast_upcast is_up) |
| apply clarsimp |
| |
| apply (intro conjI impI) |
| apply (erule_tac x="scast (t2_C.p2_C x')" in allE) |
| apply (clarsimp simp: word_not_le) |
| apply (subgoal_tac "t2_C.p2_C x' < ucast (WordArray_u32_C.len_C (heap_WordArray_u32_C s (t2_C.p1_C x')))") |
| prefer 2 |
| apply (rule unat_less_impl_less) |
| apply (simp add: unat_ucast_upcast is_up) |
| apply clarsimp |
| |
| apply (simp add: le_def[symmetric]) |
| apply (erule impE) |
| apply (rule word_le_nat_alt[THEN iffD2]) |
| apply simp |
| apply simp |
| done |
| |
| lemma u8_to_u32_corres: |
| "val_rel x x' \<Longrightarrow> |
| corres srel (App (AFun ''u8_to_u32'' []) (Var 0)) |
| (do retval \<leftarrow> u8_to_u32' x'; gets (\<lambda>_. retval) od) |
| \<xi> (x # \<gamma>) \<Xi> (Some (TPrim (Num U8)) # \<Gamma>') \<sigma> s" |
| apply (rule corres_app_abstract) |
| apply (simp add: \<xi>_def) |
| apply (simp add: u8_to_u32'_def[simplified] snd_return) |
| apply (simp add: u8_to_u32'_def u8_to_u32_def in_return val_rel_word) |
| done |
| |
| |
| lemma corres_case_t13_C_Success: |
| "\<lbrakk> x < length \<Gamma>'; |
| \<Gamma>' ! x = Some (TSum [(''Error'', TCon ''SysState'' [] Writable), |
| (''Success'', TProduct (TCon ''SysState'' [] Writable) |
| (TCon ''WordArray'' [TPrim (Num U32)] Writable))]); |
| [] \<turnstile> \<Gamma>' \<leadsto> \<Gamma>1 | \<Gamma>2; |
| val_rel (\<gamma> ! x) x'; |
| case \<gamma> ! x of |
| USum vtag vval vtyps \<Rightarrow> |
| if t13_C.tag_C x' = TAG_ENUM_Success |
| then ''Success'' = vtag \<and> val_rel vval (t13_C.Success_C x') |
| else ''Success'' \<noteq> vtag \<and> |
| val_rel (USum vtag vval [x\<leftarrow>vtyps . fst x \<noteq> ''Success'']) |
| (t123_C.Error_C_update (\<lambda>_. t13_C.Error_C x') |
| (t123_C.tag_C_update (\<lambda>_. t13_C.tag_C x') (t123_C 0 NULL))); |
| \<Xi>', [], \<Gamma>1 \<turnstile> Var x : TSum [(''Error'', TCon ''SysState'' [] Writable), |
| (''Success'', TProduct (TCon ''SysState'' [] Writable) |
| (TCon ''WordArray'' [TPrim (Num U32)] Writable))]; |
| \<Xi>', [], Some (TProduct (TCon ''SysState'' [] Writable) |
| (TCon ''WordArray'' [TPrim (Num U32)] Writable)) # \<Gamma>2 \<turnstile> match : t; |
| \<Xi>', [], Some (TSum [(''Error'', TCon ''SysState'' [] Writable)]) # \<Gamma>2 \<turnstile> not_match : t; |
| \<And>a a'. val_rel a a' \<Longrightarrow> |
| corres srel match (match' a') \<xi>' (a # \<gamma>) \<Xi>' |
| (Some (TProduct (TCon ''SysState'' [] Writable) |
| (TCon ''WordArray'' [TPrim (Num U32)] Writable)) # \<Gamma>2) \<sigma> s; |
| \<And>r r'. val_rel r r' \<Longrightarrow> |
| corres srel not_match (not_match' r') \<xi>' (r # \<gamma>) \<Xi>' |
| (Some (TSum [(''Error'', TCon ''SysState'' [] Writable)]) # \<Gamma>2) \<sigma> s |
| \<rbrakk> \<Longrightarrow> |
| corres srel |
| (Case (Var x) ''Success'' match not_match) |
| (condition (\<lambda>_. t13_C.tag_C x' = TAG_ENUM_Success) |
| (match' (t13_C.Success_C x')) |
| (do x \<leftarrow> gets (\<lambda>_. t123_C.Error_C_update (\<lambda>_. t13_C.Error_C x') |
| (t123_C.tag_C_update (\<lambda>_. t13_C.tag_C x') (t123_C 0 NULL))); |
| not_match' x od)) |
| \<xi>' \<gamma> \<Xi>' \<Gamma>' \<sigma> s" |
| apply simp |
| apply (rule corres_case |
| [where \<tau>s = "[(''Error'', TCon ''SysState'' [] Writable), |
| (''Success'', TProduct (TCon ''SysState'' [] Writable) |
| (TCon ''WordArray'' [TPrim (Num U32)] Writable))]" |
| and tag = "''Success''" and tag' = "TAG_ENUM_Success" |
| and get_tag' = "t13_C.tag_C" and get_A' = "t13_C.Success_C" |
| and wrap_rest' = "\<lambda>x'. t123_C.Error_C_update (\<lambda>_. t13_C.Error_C x') |
| (t123_C.tag_C_update (\<lambda>_. t13_C.tag_C x') (t123_C 0 NULL))" |
| , simplified]) |
| by auto |
| |
| lemma corres_case_t4_C_Success: |
| "\<lbrakk> x < length \<Gamma>'; |
| \<Gamma>' ! x = Some (TSum [(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable), |
| (''Success'', TCon ''WordArray'' [TPrim (Num U32)] Writable)]); |
| [] \<turnstile> \<Gamma>' \<leadsto> \<Gamma>1 | \<Gamma>2; |
| val_rel (\<gamma> ! x) x'; |
| case \<gamma> ! x of |
| USum vtag vval vtyps \<Rightarrow> |
| if t4_C.tag_C x' = TAG_ENUM_Success |
| then ''Success'' = vtag \<and> val_rel vval (t4_C.Success_C x') |
| else ''Success'' \<noteq> vtag \<and> |
| val_rel (USum vtag vval [x\<leftarrow>vtyps . fst x \<noteq> ''Success'']) |
| (t119_C.Error_C_update (\<lambda>_. t4_C.Error_C x') |
| (t119_C.tag_C_update (\<lambda>_. t4_C.tag_C x') (t119_C 0 NULL))); |
| \<Xi>', [], \<Gamma>1 \<turnstile> Var x : TSum [(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable), |
| (''Success'', TCon ''WordArray'' [TPrim (Num U32)] Writable)]; |
| \<Xi>', [], Some (TCon ''WordArray'' [TPrim (Num U32)] Writable) # \<Gamma>2 \<turnstile> match : t; |
| \<Xi>', [], Some (TSum [(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable)]) # \<Gamma>2 \<turnstile> not_match : t; |
| \<And>a a'. val_rel a a' \<Longrightarrow> |
| corres srel match (match' a') \<xi>' (a # \<gamma>) \<Xi>' |
| (Some (TCon ''WordArray'' [TPrim (Num U32)] Writable) # \<Gamma>2) \<sigma> s; |
| \<And>r r'. val_rel r r' \<Longrightarrow> |
| corres srel not_match (not_match' r') \<xi>' (r # \<gamma>) \<Xi>' |
| (Some (TSum [(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable)]) # \<Gamma>2) \<sigma> s |
| \<rbrakk> \<Longrightarrow> |
| corres srel (Case (Var x) ''Success'' match not_match) |
| (condition (\<lambda>_. t4_C.tag_C x' = TAG_ENUM_Success) |
| (match' (t4_C.Success_C x')) |
| (do x \<leftarrow> gets (\<lambda>_. t119_C.Error_C_update (\<lambda>_. t4_C.Error_C x') |
| (t119_C.tag_C_update (\<lambda>_. t4_C.tag_C x') (t119_C 0 NULL))); |
| not_match' x od)) |
| \<xi>' \<gamma> \<Xi>' \<Gamma>' \<sigma> s" |
| apply simp |
| apply (rule corres_case |
| [where \<tau>s = "[(''Error'', TCon ''WordArray'' [TPrim (Num U32)] Writable), |
| (''Success'', TCon ''WordArray'' [TPrim (Num U32)] Writable)]" |
| and tag = "''Success''" and tag' = "TAG_ENUM_Success" |
| and get_tag' = "t4_C.tag_C" and get_A' = "t4_C.Success_C" |
| and wrap_rest' = "\<lambda>x'. t119_C.Error_C_update (\<lambda>_. t4_C.Error_C x') |
| (t119_C.tag_C_update (\<lambda>_. t4_C.tag_C x') (t119_C 0 NULL))" |
| , simplified |
| ]) |
| by auto |
| |
| lemma corres_letbang'_4: |
| assumes split\<Gamma>: "split_bang [] is \<Gamma>' \<Gamma>1 \<Gamma>2" |
| assumes typing_x: "\<Xi>', [], \<Gamma>1 \<turnstile> x : t" |
| assumes has_kind: " [] \<turnstile> t :\<kappa> k" |
| assumes kind_escapable: "E \<in> k" |
| assumes corres_x: "corres srel x (do r1 \<leftarrow> x1'; r2 \<leftarrow> x2' r1; r3 \<leftarrow> x3' r1 r2; x4' r1 r2 r3 od) \<xi>' \<gamma> \<Xi>' \<Gamma>1 \<sigma> s" |
| assumes corres_cont: "\<And>v v' \<sigma>' s'. val_rel v (v'::'a::cogent_C_val) \<Longrightarrow> |
| corres srel y (y' v') \<xi>' (v # \<gamma>) \<Xi>' (Some t # \<Gamma>2) \<sigma>' s'" |
| shows "corres srel (LetBang is x y) |
| (do r1 \<leftarrow> x1'; r2 \<leftarrow> x2' r1; r3 \<leftarrow> x3' r1 r2; r4 \<leftarrow> x4' r1 r2 r3; y' r4 od) \<xi>' \<gamma> \<Xi>' \<Gamma>' \<sigma> s" |
| using assms |
| corres_letbang[where |
| x'="do r1 \<leftarrow> x1'; r2 \<leftarrow> x2' r1; r3 \<leftarrow> x3' r1 r2; x4' r1 r2 r3 od", |
| simplified bind_assoc] |
| by blast |
| |
| (* Top-level proof *) |
| lemma caller_corres: |
| "val_rel a a' \<Longrightarrow> |
| corres state_rel caller (caller' a') \<xi> [a] \<Xi> [Some (fst (snd caller_type))] \<sigma> s" |
| apply (simp only: fst_conv snd_conv caller_def caller'_def caller_type_def) |
| apply (subst return_exn_simp) |
| apply (subst guard_True_bind)+ |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_var) |
| apply simp |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) back |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_lit) |
| apply (simp add: val_rel_word) |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_cast) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply simp |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) back |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_tuple) |
| apply (simp add: val_rel_t11_C_def) |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) back |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule wordarray_create_0_corres) |
| apply simp |
| apply (subst gets_to_return, subst bind_return) back back back back back back back |
| apply (rule corres_case_t13_C_Success) |
| apply simp |
| apply simp |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply simp |
| apply (fastforce simp: val_rel_t13_C_def val_rel_t123_C_def TAG_ENUM_Error_def TAG_ENUM_Success_def) |
| apply (simp, tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (simp, tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_split_lazy[where ?p1.0="t12_C.p1_C" and ?p2.0="t12_C.p2_C"]) |
| apply simp |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (simp add: val_rel_t12_C_def) |
| apply simp |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (simp, tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_lit) |
| apply (simp add: val_rel_word) |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) back |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule u8_to_u32_corres) |
| apply simp |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_lit) |
| apply (simp add: val_rel_word) |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule u8_to_u32_corres) |
| apply simp |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_struct[where xs="[5,2,0]", simplified, folded gets_to_return]) |
| apply (simp add: val_rel_t3_C_def) |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule wordarray_put_0_corres) |
| apply simp |
| apply (rule corres_case_t4_C_Success) |
| apply simp |
| apply simp |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply simp |
| apply (fastforce simp: val_rel_t4_C_def val_rel_t119_C_def TAG_ENUM_Success_def TAG_ENUM_Error_def) |
| apply (simp, tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (simp, tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_letbang'_4) |
| apply (simp, tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply simp |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) back |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_lit) |
| apply (simp add: val_rel_word) |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) back |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_cast) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply simp |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) back |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_tuple) |
| apply (simp add: val_rel_t2_C_def) |
| apply (rule wordarray_get_0_corres) |
| apply simp |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) back |
| apply (simp, tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_tuple) |
| apply (simp add: val_rel_t12_C_def) |
| apply (rule wordarray_free_0_corres) |
| apply simp |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule_tac get_val'=t119_C.Error_C in corres_esac) |
| apply simp |
| apply simp |
| apply simp |
| apply (clarsimp simp: val_rel_t119_C_def) |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) back |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule corres_tuple) |
| apply (simp add: val_rel_t12_C_def) |
| apply (rule wordarray_free_0_corres) |
| apply simp |
| apply (rule corres_let) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (tactic {* map (fn t => rtac t 1) caller_typing_bucket |> APPEND_LIST *}) |
| apply (rule_tac get_val'=t123_C.Error_C in corres_esac) |
| apply simp |
| apply simp |
| apply simp |
| apply (clarsimp simp: val_rel_t123_C_def) |
| apply (rule corres_var) |
| apply simp |
| done |
| |
| (* ghetto find_theorems template *) |
| ML {* |
| caller_typing_bucket |
| |> filter (fn t => |
| Pattern.matches_subterm @{theory} |
| (Proof_Context.read_term_pattern @{context} |
| "_, _, _ \<turnstile> Split _ _ : _", |
| prop_of t)) |
| *} |
| |
| end |
| |
| end |
