equal
deleted
inserted
replaced
1950 @{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\ |
1950 @{text "\<forall>x. t = Var x \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>a t'. t = Lam a t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\ |
1951 @{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\ |
1951 @{text "\<forall>t\<^isub>1 t\<^isub>2. t = App t\<^isub>1 t\<^isub>2 \<Rightarrow> P\<^bsub>trm\<^esub>"} & @{text "\<forall>p t'. t = Let p t' \<Rightarrow> P\<^bsub>trm\<^esub>"}\\ |
1952 \end{array}} |
1952 \end{array}} |
1953 \end{equation} |
1953 \end{equation} |
1954 % |
1954 % |
1955 These cases lemmas have a premise for auch term-constructor. |
1955 These cases lemmas have a premise for each term-constructor. |
1956 The idea behind them is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"}, |
1956 The idea behind them is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"}, |
1957 provided we can show that this property holds if we substitute for @{text "t"} all |
1957 provided we can show that this property holds if we substitute for @{text "t"} all |
1958 possible term-constructors. |
1958 possible term-constructors. |
1959 |
1959 |
1960 The only remaining difficulty is that in order to derive the stronger induction |
1960 The only remaining difficulty is that in order to derive the stronger induction |
2004 % |
2004 % |
2005 Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that |
2005 Now Properties \ref{supppermeq} and \ref{avoiding} give us a permutation @{text q} such that |
2006 @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"} |
2006 @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"} |
2007 is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. But |
2007 is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. But |
2008 these facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This |
2008 these facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This |
2009 completes the interesting cases in \eqref{letpat} for stregthening the induction |
2009 completes the interesting cases in \eqref{letpat} for strengthening the induction |
2010 principles. |
2010 principles. |
2011 |
2011 |
2012 |
2012 |
2013 |
2013 |
2014 %A natural question is |
2014 %A natural question is |