11 ML {* |
11 ML {* |
12 fun prove_perm_empty lthy induct perm_def perm_frees = |
12 fun prove_perm_empty lthy induct perm_def perm_frees = |
13 let |
13 let |
14 val perm_types = map fastype_of perm_frees; |
14 val perm_types = map fastype_of perm_frees; |
15 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
15 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
|
16 fun glc ((perm, T), x) = |
|
17 HOLogic.mk_eq (perm $ @{term "0 :: perm"} $ Free (x, T), Free (x, T)) |
16 val gl = |
18 val gl = |
17 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
19 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
18 (map (fn ((perm, T), x) => HOLogic.mk_eq |
20 (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))); |
19 (perm $ @{term "0 :: perm"} $ Free (x, T), |
|
20 Free (x, T))) |
|
21 (perm_frees ~~ |
|
22 map body_type perm_types ~~ perm_indnames))); |
|
23 fun tac _ = |
21 fun tac _ = |
24 EVERY [ |
22 EVERY [ |
25 indtac induct perm_indnames 1, |
23 indtac induct perm_indnames 1, |
26 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) |
24 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) |
27 ]; |
25 ]; |
36 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
34 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
37 val pi1 = Free ("pi1", @{typ perm}); |
35 val pi1 = Free ("pi1", @{typ perm}); |
38 val pi2 = Free ("pi2", @{typ perm}); |
36 val pi2 = Free ("pi2", @{typ perm}); |
39 val perm_types = map fastype_of perm_frees |
37 val perm_types = map fastype_of perm_frees |
40 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
38 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
|
39 fun glc ((perm, T), x) = |
|
40 HOLogic.mk_eq ( |
|
41 perm $ (add_perm $ pi1 $ pi2) $ Free (x, T), |
|
42 perm $ pi1 $ (perm $ pi2 $ Free (x, T))) |
41 val gl = |
43 val gl = |
42 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
44 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
43 (map (fn ((perm, T), x) => |
45 (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) |
44 let |
|
45 val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) |
|
46 val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T)) |
|
47 in HOLogic.mk_eq (lhs, rhs) |
|
48 end) |
|
49 (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) |
|
50 fun tac _ = |
46 fun tac _ = |
51 EVERY [ |
47 EVERY [ |
52 indtac induct perm_indnames 1, |
48 indtac induct perm_indnames 1, |
53 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) |
49 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) |
54 ] |
50 ] |