equal
deleted
inserted
replaced
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 assumes a1: "\<And>name b. P b (Var name)" |
62 assumes a1: "\<And>name b. P b (Var name)" |
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)" |
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 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)" |
64 and a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)" |
65 shows "P a t" |
65 shows "P a t \<and> P' d ts " |
66 proof - |
66 proof - |
67 have "\<And>p. P a (p \<bullet> t)" |
67 have " (\<forall>p. P a (p \<bullet> t)) \<and> (\<forall>p. P' d (p \<bullet> ts))" |
68 apply (induct t rule: t_tyS.inducts(1)) |
68 apply (rule t_tyS.induct) |
69 apply (simp add: a1) |
69 apply (simp add: a1) |
70 apply (simp_all) |
70 apply (simp_all) |
71 apply (rule_tac ?t1.0="p \<bullet> t1" and ?t2.0="p \<bullet> t2" in a2) |
71 apply (rule allI) |
|
72 apply (rule a2) |
|
73 defer defer |
|
74 apply (rule allI) |
|
75 apply (rule a3) |
|
76 apply simp_all |
72 sorry |
77 sorry |
73 then have "P a (0 \<bullet> t)" by blast |
78 then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast |
74 then show "P a t" by simp |
79 then show ?thesis by simp |
75 qed |
80 qed |
76 |
81 |
77 lemma |
82 lemma |
78 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
83 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
79 apply(simp add: t_tyS.eq_iff) |
84 apply(simp add: t_tyS.eq_iff) |