equal
deleted
inserted
replaced
57 done |
57 done |
58 |
58 |
59 lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS] |
59 lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS] |
60 |
60 |
61 lemma induct: |
61 lemma induct: |
62 "\<lbrakk>\<And>name b. P b (Var name); |
62 assumes a1: "\<And>name b. P b (Var name)" |
63 \<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2); |
63 and a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)" |
64 \<And>fset t. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t) |
64 and a3: "\<And>fset t. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |
65 \<rbrakk> \<Longrightarrow> P a t" |
65 shows "P a t" |
66 oops |
66 proof - |
67 |
67 have "\<And>p. P a (p \<bullet> t)" |
|
68 apply (induct t rule: t_tyS.inducts(1)) |
|
69 apply (simp add: a1) |
|
70 apply (simp_all) |
|
71 apply (rule_tac ?t1.0="p \<bullet> t1" and ?t2.0="p \<bullet> t2" in a2) |
|
72 sorry |
|
73 then have "P a (0 \<bullet> t)" by blast |
|
74 then show "P a t" by simp |
|
75 qed |
68 |
76 |
69 lemma |
77 lemma |
70 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
78 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
71 apply(simp add: t_tyS.eq_iff) |
79 apply(simp add: t_tyS.eq_iff) |
72 apply(rule_tac x="0::perm" in exI) |
80 apply(rule_tac x="0::perm" in exI) |