equal
deleted
inserted
replaced
16 lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)" |
16 lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)" |
17 apply (induct_tac ts rule: rev_induct) |
17 apply (induct_tac ts rule: rev_induct) |
18 apply auto |
18 apply auto |
19 done |
19 done |
20 |
20 |
21 lemma Var_eq_apps_conv [rulified, iff]: |
21 lemma Var_eq_apps_conv [rule_format, iff]: |
22 "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])" |
22 "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])" |
23 apply (induct_tac ss) |
23 apply (induct_tac ss) |
24 apply auto |
24 apply auto |
25 done |
25 done |
26 |
26 |
27 lemma Var_apps_eq_Var_apps_conv [rulified, iff]: |
27 lemma Var_apps_eq_Var_apps_conv [rule_format, iff]: |
28 "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)" |
28 "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)" |
29 apply (induct_tac rs rule: rev_induct) |
29 apply (induct_tac rs rule: rev_induct) |
30 apply simp |
30 apply simp |
31 apply blast |
31 apply blast |
32 apply (rule allI) |
32 apply (rule allI) |
67 "\<forall>s t. Abs s $ t ~= Var n $$ ss" |
67 "\<forall>s t. Abs s $ t ~= Var n $$ ss" |
68 apply (induct_tac ss rule: rev_induct) |
68 apply (induct_tac ss rule: rev_induct) |
69 apply auto |
69 apply auto |
70 done |
70 done |
71 |
71 |
72 lemma Var_apps_neq_Abs_apps [rulified, iff]: |
72 lemma Var_apps_neq_Abs_apps [rule_format, iff]: |
73 "\<forall>ts. Var n $$ ts ~= Abs r $$ ss" |
73 "\<forall>ts. Var n $$ ts ~= Abs r $$ ss" |
74 apply (induct_tac ss rule: rev_induct) |
74 apply (induct_tac ss rule: rev_induct) |
75 apply simp |
75 apply simp |
76 apply (rule allI) |
76 apply (rule allI) |
77 apply (induct_tac ts rule: rev_induct) |
77 apply (induct_tac ts rule: rev_induct) |
101 done |
101 done |
102 |
102 |
103 |
103 |
104 text {* \medskip A customized induction schema for @{text "$$"}. *} |
104 text {* \medskip A customized induction schema for @{text "$$"}. *} |
105 |
105 |
106 lemma lem [rulified (no_asm)]: |
106 lemma lem [rule_format (no_asm)]: |
107 "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts); |
107 "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts); |
108 !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts) |
108 !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts) |
109 |] ==> \<forall>t. size t = n --> P t" |
109 |] ==> \<forall>t. size t = n --> P t" |
110 proof - |
110 proof - |
111 case antecedent |
111 case antecedent |