header {* Representing Intensional Logic  *}

theory Intensional 
imports Main 
begin

text {* Intensional is a generic theory allowing lifting of types.
*}

axclass 
  world \<subseteq> type
text {*
@{term world} is a type class of possible worlds. It is a subclass
of all HOL types @{term type}. No axioms are provided, since its only
purpose is to avoid silly use of the @{term Intensional} syntax. *}


section{* Abstract Syntax *}


types
  ('w,'a) expr = "'w \<Rightarrow> 'a"              
  'w form = "('w, bool) expr"
text {* The intention is that @{typ 'a} will be used for unliftet 
types (class @{term type}), while @{typ 'w} is liftet (class @{term world}). 
*}

consts
  Valid    :: "('w::world) form \<Rightarrow> bool"
  const    :: "'a \<Rightarrow> ('w::world, 'a) expr"
  lift     :: "['a \<Rightarrow> 'b, ('w::world, 'a) expr] \<Rightarrow> ('w,'b) expr"
  lift2    :: "['a \<Rightarrow> 'b \<Rightarrow> 'c, ('w::world,'a) expr, ('w,'b) expr] \<Rightarrow> ('w,'c) expr"
  lift3    :: "['a \<Rightarrow> 'b => 'c \<Rightarrow> 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] \<Rightarrow> ('w,'d) expr"
  lift4    :: "['a \<Rightarrow> 'b => 'c \<Rightarrow> 'd \<Rightarrow> 'e, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr,('w,'d) expr] \<Rightarrow> ('w,'e) expr"
text{* @{term "Valid F"} asserts that the lifted formula @{term F} holds everywhere. @{term const} allows
 lifting of a constant, while @{term lift}, @{term lift2} and  @{term lift3} allows lifting of functions
 with arity 1,2 and 3 respectively.*}

consts
  RAll     :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"      (binder "Rall " 10)
  REx      :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"      (binder "Rex " 10)
  REx1     :: "('a \<Rightarrow> ('w::world) form) \<Rightarrow> 'w form"      (binder "Rex! " 10)
text{* @{term RAll}, @{term REx} and @{term REx1} introduces "rigid" quantification on logical
  level. @{term RAll} is universal quantification, @{term REx} is existential quantifcatoin while
  @{term REx1} requires one and only one witness. *}

section{* Concrete Syntax *}

nonterminals
  lift
  liftargs
text{* @{term lift} is introduced of lifted expressions. The idea is to use Isabelle's
macro mechanism to convert between the concrete and abstract syntax. *}

syntax
  ""            :: "id \<Rightarrow> lift"                          ("_")
  ""            :: "longid \<Rightarrow> lift"                      ("_")
  ""            :: "var \<Rightarrow> lift"                         ("_")
  "_applC"      :: "[lift, cargs] \<Rightarrow> lift"               ("(1_/ _)" [1000, 1000] 999)
  ""            :: "lift \<Rightarrow> lift"                        ("'(_')")
  "_lambda"     :: "[idts, 'a] \<Rightarrow> lift"                  ("(3%_./ _)" [0, 3] 3)
  "_constrain"  :: "[lift, type] \<Rightarrow> lift"                ("(_::_)" [4, 0] 3)
  ""            :: "lift \<Rightarrow> liftargs"                    ("_")
  "_liftargs"   :: "[lift, liftargs] \<Rightarrow> liftargs"        ("_,/ _")
  "_Valid"      :: "lift \<Rightarrow> bool"                        ("(|- _)" 5)
  "_holdsAt"    :: "['a, lift] \<Rightarrow> bool"                  ("(_ |= _)" [100,10] 10)

  (* Syntax for lifted expressions outside the scope of \<turnstile> or \<Turnstile>.*)
  "LIFT"        :: "lift \<Rightarrow> 'a"                          ("LIFT _")

  (* generic syntax for lifted constants and functions *)
  "_const"      :: "'a \<Rightarrow> lift"                          ("(#_)" [1000] 999)
  "_lift"       :: "['a, lift] \<Rightarrow> lift"                  ("(_<_>)" [1000] 999)
  "_lift2"      :: "['a, lift, lift] \<Rightarrow> lift"            ("(_<_,/ _>)" [1000] 999)
  "_lift3"      :: "['a, lift, lift, lift] \<Rightarrow> lift"      ("(_<_,/ _,/ _>)" [1000] 999)
  "_lift4"      :: "['a, lift, lift, lift,lift] \<Rightarrow> lift"      ("(_<_,/ _,/ _,/ _>)" [1000] 999)

  (* concrete syntax for common infix functions: reuse same symbol *)
  "_liftEqu"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ =/ _)" [50,51] 50)
  "_liftNeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ ~=/ _)" [50,51] 50)
  "_liftNot"    :: "lift \<Rightarrow> lift"                        ("(~ _)" [40] 40)
  "_liftAnd"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ &/ _)" [36,35] 35)
  "_liftOr"     :: "[lift, lift] \<Rightarrow> lift"                ("(_ |/ _)" [31,30] 30)
  "_liftImp"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ -->/ _)" [26,25] 25)
  "_liftIf"     :: "[lift, lift, lift] \<Rightarrow> lift"          ("(if (_)/ then (_)/ else (_))" 10)
  "_liftPlus"   :: "[lift, lift] \<Rightarrow> lift"                ("(_ +/ _)" [66,65] 65)
  "_liftMinus"  :: "[lift, lift] \<Rightarrow> lift"                ("(_ -/ _)" [66,65] 65)
  "_liftTimes"  :: "[lift, lift] \<Rightarrow> lift"                ("(_ */ _)" [71,70] 70)
  "_liftDiv"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ div _)" [71,70] 70)
  "_liftMod"    :: "[lift, lift] \<Rightarrow> lift"                ("(_ mod _)" [71,70] 70)
  "_liftLess"   :: "[lift, lift] \<Rightarrow> lift"                ("(_/ < _)"  [50, 51] 50)
  "_liftLeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ <= _)" [50, 51] 50)
  "_liftMem"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ : _)" [50, 51] 50)
  "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift"                ("(_/ ~: _)" [50, 51] 50)
  "_liftFinset" :: "liftargs => lift"                    ("{(_)}")
  (** TODO: syntax for lifted collection / comprehension **)
  "_liftPair"   :: "[lift,liftargs] \<Rightarrow> lift"                   ("(1'(_,/ _'))")
  (* infix syntax for list operations *)
  "_liftCons" :: "[lift, lift] \<Rightarrow> lift"                  ("(_ #/ _)" [65,66] 65)
  "_liftApp"  :: "[lift, lift] \<Rightarrow> lift"                  ("(_ @/ _)" [65,66] 65)
  "_liftList" :: "liftargs \<Rightarrow> lift"                      ("[(_)]")

  (* Rigid quantification (syntax level) *)
  "_ARAll"  :: "[idts, lift] \<Rightarrow> lift"                    ("(3! _./ _)" [0, 10] 10)
  "_AREx"   :: "[idts, lift] \<Rightarrow> lift"                    ("(3? _./ _)" [0, 10] 10)
  "_AREx1"  :: "[idts, lift] \<Rightarrow> lift"                    ("(3?! _./ _)" [0, 10] 10)
  "_RAll" :: "[idts, lift] \<Rightarrow> lift"                      ("(3ALL _./ _)" [0, 10] 10)
  "_REx"  :: "[idts, lift] \<Rightarrow> lift"                      ("(3EX _./ _)" [0, 10] 10)
  "_REx1" :: "[idts, lift] \<Rightarrow> lift"                      ("(3EX! _./ _)" [0, 10] 10)

translations
  "_const"        \<rightleftharpoons>  "const"
  "_lift"         \<rightleftharpoons> "lift"
  "_lift2"        \<rightleftharpoons> "lift2"
  "_lift3"        \<rightleftharpoons> "lift3"
  "_lift4"        \<rightleftharpoons> "lift4"
  "_Valid"        \<rightleftharpoons> "Valid"
  "_RAll x A"     \<rightleftharpoons> "Rall x. A"
  "_REx x A"      \<rightleftharpoons> "Rex x. A"
  "_REx1 x A"     \<rightleftharpoons> "Rex! x. A"
  "_ARAll"        \<rightharpoonup>  "_RAll"
  "_AREx"         \<rightharpoonup> "_REx"
  "_AREx1"        \<rightharpoonup> "_REx1"

  "w |= A"        \<rightharpoonup> "A w"
  "LIFT A"        \<rightharpoonup> "A::_\<Rightarrow>_"

  "_liftEqu"      \<rightleftharpoons> "_lift2 (op =)"
  "_liftNeq u v"  \<rightleftharpoons> "_liftNot (_liftEqu u v)"
  "_liftNot"      \<rightleftharpoons> "_lift Not"
  "_liftAnd"      \<rightleftharpoons> "_lift2 (op &)"
  "_liftOr"       \<rightleftharpoons> "_lift2 (op | )"
  "_liftImp"      \<rightleftharpoons> "_lift2 (op -->)"
  "_liftIf"       \<rightleftharpoons> "_lift3 If"
  "_liftPlus"     \<rightleftharpoons> "_lift2 (op +)"
  "_liftMinus"    \<rightleftharpoons> "_lift2 (op -)"
  "_liftTimes"    \<rightleftharpoons> "_lift2 (op *)"
  "_liftDiv"      \<rightleftharpoons> "_lift2 (op div)"
 "_liftMod"      \<rightleftharpoons> "_lift2 (op mod)"
  "_liftLess"     \<rightleftharpoons> "_lift2 (op <)"
  "_liftLeq"      \<rightleftharpoons> "_lift2 (op <=)"
  "_liftMem"      \<rightleftharpoons> "_lift2 (op :)"
  "_liftNotMem x xs"             \<rightleftharpoons> "_liftNot (_liftMem x xs)"
  "_liftFinset (_liftargs x xs)" \<rightleftharpoons> "_lift2 insert x (_liftFinset xs)"
  "_liftFinset x"                \<rightleftharpoons> "_lift2 insert x (_const {})"
  "_liftPair x (_liftargs y z)"  \<rightleftharpoons> "_liftPair x (_liftPair y z)"
  "_liftPair"                    \<rightleftharpoons> "_lift2 Pair"
  "_liftCons"                    \<rightleftharpoons> "lift2 Cons"
  "_liftApp"                     \<rightleftharpoons> "lift2 (op @)"
  "_liftList (_liftargs x xs)"   \<rightleftharpoons> "_liftCons x (_liftList xs)"
  "_liftList x"                  \<rightleftharpoons> "_liftCons x (_const [])"

  "w |= ~A"       \<leftharpoondown>  "_liftNot A w"
  "w |=  A & B"   \<leftharpoondown> "_liftAnd A B w"
  "w |= A | B"    \<leftharpoondown> "_liftOr A B w"
  "w |= A --> B"  \<leftharpoondown> "_liftImp A B w"
  "w |= u = v"    \<leftharpoondown> "_liftEqu u v w"
  "w |= ALL x. A" \<leftharpoondown> "_RAll x A w"
  "w |= EX x. A"  \<leftharpoondown> "_REx x A w"
  "w |= EX! x. A" \<leftharpoondown> "_REx1 x A w"

syntax (xsymbols)
  "_Valid"      :: "lift \<Rightarrow> bool"                        ("(\<turnstile> _)" 5)
  "_holdsAt"    :: "['a, lift] \<Rightarrow> bool"                  ("(_ \<Turnstile> _)" [100,10] 10)
  "_liftNeq"    :: "[lift, lift] \<Rightarrow> lift"                (infixl "\<noteq>" 50)
  "_liftNot"    :: "lift \<Rightarrow> lift"                        ("\<not> _" [40] 40)
  "_liftAnd"    :: "[lift, lift] \<Rightarrow> lift"                (infixr "\<and>" 35)
  "_liftOr"     :: "[lift, lift] \<Rightarrow> lift"                (infixr "\<or>" 30)
  "_liftImp"    :: "[lift, lift] \<Rightarrow> lift"                (infixr "\<longrightarrow>" 25)
  "_RAll"       :: "[idts, lift] \<Rightarrow> lift"                ("(3\<forall>_./ _)" [0, 10] 10)
  "_REx"        :: "[idts, lift] \<Rightarrow> lift"                ("(3\<exists>_./ _)" [0, 10] 10)
  "_REx1"       :: "[idts, lift] \<Rightarrow> lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
  "_liftLeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<le> _)" [50, 51] 50)
  "_liftMem"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<in> _)" [50, 51] 50)
  "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<notin> _)" [50, 51] 50)

syntax (HTML output)
  "_liftNeq"    :: "[lift, lift] \<Rightarrow> lift"                (infixl "\<noteq>" 50)
  "_liftNot"    :: "lift \<Rightarrow> lift"                        ("\<not> _" [40] 40)
  "_liftAnd"    :: "[lift, lift] \<Rightarrow> lift"                (infixr "\<and>" 35)
  "_liftOr"     :: "[lift, lift] \<Rightarrow> lift"                (infixr "\<or>" 30)
  "_RAll"       :: "[idts, lift] \<Rightarrow> lift"                ("(3\<forall>_./ _)" [0, 10] 10)
  "_REx"        :: "[idts, lift] \<Rightarrow> lift"                ("(3\<exists>_./ _)" [0, 10] 10)
  "_REx1"       :: "[idts, lift] \<Rightarrow> lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
  "_liftLeq"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<le> _)" [50, 51] 50)
  "_liftMem"    :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<in> _)" [50, 51] 50)
  "_liftNotMem" :: "[lift, lift] \<Rightarrow> lift"                ("(_/ \<notin> _)" [50, 51] 50)


section {* Definitions *}

defs
  Valid_def:   "|- A    ==  ALL w. w |= A"
  unl_con:     "LIFT #c w  ==  c"
  unl_lift:    "LIFT f<x> w == f (x w)"
  unl_lift2:   "LIFT f<x, y> w == f (x w) (y w)"
  unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"
  unl_lift4:   "LIFT f<x, y, z, zz> w == f (x w) (y w) (z w) (zz w)"

(* Cannot use defs here - must look into *)
axioms
  unl_Rall:    "w \<Turnstile> ALL x. A x  ==  ALL x. (w \<Turnstile> A x)"
  unl_Rex:     "w \<Turnstile> EX x. A x   ==  EX x. (w \<Turnstile> A x)"
  unl_Rex1:    "w \<Turnstile> EX! x. A x  ==  EX! x. (w \<Turnstile> A x)"

section {* Lemmas and Tactics *}

lemma intD[dest]: "\<turnstile> A \<Longrightarrow> w \<Turnstile> A"
proof -
  assume a:"\<turnstile> A"
  from a have "ALL w. w \<Turnstile> A" by (auto simp add: Valid_def)
  thus ?thesis ..
qed

lemma intI[simp]: assumes P1:"(\<And> w. w \<Turnstile> A)" shows "\<turnstile> A"
proof -
  fix w
  from P1 have "A w" by blast
  thus ?thesis by (auto simp add: Valid_def)
qed

lemma inteq_reflection[simp]: assumes P1: "\<turnstile> x=y" shows  "(x \<equiv> y)"
proof -
  from P1 have "ALL w. w |= x=y" by (unfold Valid_def)
  hence P2: "ALL w. x w = y w" by (unfold unl_lift2)
  hence P3:"x=y"
  proof -
    from P2 have "\<And> w. x w = y w" ..
    thus ?thesis by (rule ext)
  qed
  thus "x \<equiv> y" by (rule "eq_reflection")
qed

lemma int_simps1 [simp]:  "|- (x=x) = #True"
by (simp add: Valid_def unl_lift2 unl_con)

lemma int_simps2 [simp]:  "\<turnstile> (\<not> #True) = #False"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps3 [simp]:  "\<turnstile> (\<not> #False) = #True"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps4 [simp]:  "\<turnstile> (\<not>\<not> P) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps5 [simp]:  "\<turnstile> ((\<not> P) = P) = #False"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps6 [simp]: "\<turnstile> (P = (\<not>P)) = #False"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps7 [simp]:  "\<turnstile> (P \<noteq> Q) = (P = (\<not> Q))"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps8 [simp]:  "\<turnstile> (#True=P) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps9 [simp]:  "\<turnstile> (P=#True) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps10 [simp]:  "\<turnstile> (#True \<longrightarrow> P) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps11 [simp]:  "\<turnstile> (#False \<longrightarrow> P) = #True"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps12 [simp]:  "\<turnstile> (P \<longrightarrow> #True) = #True"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps13 [simp]:  "\<turnstile> (P \<longrightarrow> P) = #True"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps14 [simp]:  "\<turnstile> (P \<longrightarrow> #False) = (\<not>P)"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps15 [simp]:  "\<turnstile> (P \<longrightarrow> ~P) = (\<not>P)"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps16 [simp]:  "\<turnstile> (P \<and> #True) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps17 [simp]:  "\<turnstile> (#True \<and> P) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps18 [simp]:  "\<turnstile> (P \<and> #False) = #False"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps19 [simp]:  "\<turnstile> (#False \<and> P) = #False"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps20 [simp]:  "\<turnstile> (P \<and> P) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps21 [simp]:  "\<turnstile> (P \<and> ~P) = #False"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps22 [simp]: "\<turnstile> (\<not>P \<and> P) = #False"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps23 [simp]: "\<turnstile> (P \<or> #True) = #True"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps24 [simp]: "\<turnstile> (#True \<or> P) = #True"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps25 [simp]: "\<turnstile> (P \<or> #False) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps26 [simp]: "\<turnstile> (#False \<or> P) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps27 [simp]: "\<turnstile> (P \<or> P) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps28 [simp]: "\<turnstile> (P \<or> \<not>P) = #True"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps29 [simp]: "\<turnstile> (\<not>P \<or> P) = #True"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps30 [simp]:  "\<turnstile> (\<forall> x. P) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con unl_Rall)

lemma int_simps31 [simp]:  "\<turnstile> (\<exists> x. P) = P"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con unl_Rex)

lemma int_simps32 [simp]:  "\<turnstile> (\<not>Q \<longrightarrow> \<not>P) = (P \<longrightarrow> Q)"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemma int_simps33 [simp]:  "\<turnstile> (P \<or> Q \<longrightarrow> R) = ((P \<longrightarrow> R) \<and> (Q \<longrightarrow> R))"
by (auto simp add: Valid_def unl_lift2 unl_lift unl_con)

lemmas int_simps = int_simps1 int_simps2 int_simps3 int_simps4 int_simps5
                   int_simps6 int_simps7 int_simps8 int_simps9 int_simps10
                   int_simps11 int_simps12 int_simps13 int_simps14 int_simps15
                   int_simps16 int_simps17 int_simps18 int_simps19 int_simps20
                   int_simps21 int_simps22 int_simps23 int_simps24 int_simps25
                   int_simps26 int_simps27 int_simps28 int_simps29 int_simps30
                   int_simps31 int_simps32 int_simps33

lemma Not_Rall: "\<turnstile> (\<not>(\<forall> x. F x)) = (\<exists> x. \<not>F x)"
proof -
 have "\<forall> w. w \<Turnstile> ((\<not> (\<forall> x. F x)) = (\<exists>x. \<not> F x))"
 proof
   fix w
   have s1: "w \<Turnstile> (\<not> (\<forall> x. F x)) \<Longrightarrow> w \<Turnstile> (\<exists>x. \<not> F x)" 
   proof -
     assume a1: "w \<Turnstile> (\<not> (\<forall> x. F x))"
     hence "\<not> RAll F w" by (unfold unl_lift)
     hence "\<not> (\<forall>x. F x w)" by (unfold unl_Rall)
     hence "\<exists>x. w \<Turnstile> \<not> F x" by (simp add: unl_Rex unl_lift)
     thus ?thesis by (unfold unl_Rex)
   qed
   moreover
   have s2: "w \<Turnstile> (\<exists>x. \<not> F x) \<Longrightarrow> w \<Turnstile> \<not> RAll F" 
   proof -
     assume a2: "w \<Turnstile> (\<exists>x. \<not> F x)"
     hence "\<exists> x. w \<Turnstile> \<not> F x" by (unfold unl_Rex)
     hence "\<exists> x. \<not> F x w" by (unfold unl_lift)
     hence "\<not> (\<forall>x. F x w)" by simp
     hence "\<not> RAll F w" by (unfold unl_Rall)
     thus "w \<Turnstile> \<not> RAll F" by (unfold unl_lift)
   qed
   ultimately have "(w \<Turnstile> \<not> RAll F) = (w \<Turnstile> (\<exists>x. \<not> F x))" ..
   thus "w \<Turnstile> ((\<not> (\<forall> x. F x)) = (\<exists>x. \<not> F x))" by (unfold unl_lift2)
   qed
   thus ?thesis by (unfold Valid_def)
qed

lemma Not_Rex: "\<turnstile> (\<not>(\<exists> x. F x)) = (\<forall> x. \<not>F x)"
proof -
  have "\<forall> w. w \<Turnstile> ((\<not> REx F) = (\<forall> x. \<not> F x))"
  proof
    fix w
    have l2r: "(w \<Turnstile> (\<not> REx F)) \<Longrightarrow> (w \<Turnstile> (\<forall> x. \<not> F x))"
    proof -
      assume l2a1: "(w \<Turnstile> (\<not> REx F))"
      from l2a1 have  "\<not> (\<exists> x. F x w)" by (simp add: unl_Rex unl_lift)
      hence  "\<forall> x. (\<not> F x w)" by simp
      hence "\<forall> x. (w \<Turnstile> \<not> F x)" by (auto simp add: unl_lift)
      thus "w \<Turnstile> (\<forall> x. \<not> F x)" by (unfold unl_Rall)
    qed
    moreover
    have r2l: "(w \<Turnstile> (\<forall> x. \<not> F x)) \<Longrightarrow>  (w \<Turnstile> (\<not> REx F))"
    proof -
      assume l2a1: "(w \<Turnstile> (\<forall> x. \<not> F x))"
      hence "\<forall> x. (w \<Turnstile> \<not> F x)" by (unfold unl_Rall)
      hence "\<forall> x. (\<not> F x w)" by (unfold unl_lift)
      hence "\<not> (\<exists> x. F x w)" by (simp add: unl_Rex unl_lift)
      thus ?thesis by (simp add: unl_Rex unl_lift)
    qed
    ultimately have "(w \<Turnstile> (\<not> REx F)) = (w \<Turnstile> (\<forall> x. \<not> F x))" ..
    thus "w \<Turnstile> (\<not> REx F) = (\<forall> x. \<not> F x)" by (unfold unl_lift2)
  qed
  thus ?thesis by (unfold Valid_def)
qed

lemma TrueW: "\<turnstile> #True"
proof -
 have "\<forall> w. True" by blast
 hence "\<forall> w. w \<Turnstile> (#True)" by (unfold unl_con)
 thus ?thesis by (unfold Valid_def)
qed

lemmas intensional_rews[simp] = unl_con unl_lift unl_lift2 unl_lift3 unl_lift4 unl_Rall unl_Rex unl_Rex1 

subsection {* Functions to \emph{unlift} intensional implications into HOL rules *}

text{*
 Basic unlifting introduces a parameter @{term w} and applies basic rewrites, e.g 
 @{term "\<turnstile> F = G"} becomes @{term "F w = G w"} and @{term "\<turnstile> F \<longrightarrow> G"} becomes   
 @{term "F w \<longrightarrow> G w"}.
*}
method_setup int_unlift = 
{*
let 
  fun int_unlift_tac args ctxt = 
      let val intensional_rews = ProofContext.get_thms ctxt (PureThy.Name "intensional_rews")
          val intI = ProofContext.get_thm ctxt (PureThy.Name "intI")
      in 
        (Method.METHOD (fn chained_facts => 
           (fn th => 
           Seq.single (rewrite_rule intensional_rews ((intI RS th) handle _ => th)))))
      end
in 
  int_unlift_tac 
end
*} "int_unlift tactic lifted to being a method."

lemma int_eq: "\<turnstile> X = Y \<Longrightarrow> X = Y"
  by auto

lemma int_iffI: assumes h1: "\<turnstile> F \<longrightarrow> G"
                 and   h2: "\<turnstile> G \<longrightarrow> F"
                shows      "\<turnstile> F = G"
proof (int_unlift,rule iffI)
  fix w
  assume "w \<Turnstile> F"
  with h1[THEN intD] show "w \<Turnstile> G" by auto
next
  fix w
  assume "w \<Turnstile> G"
  with h2[THEN intD] show "w \<Turnstile> F" by auto
qed

lemma int_iffD1: assumes h: "\<turnstile> F = G"
  shows "\<turnstile> F \<longrightarrow> G"
  using h[THEN intD] by auto

lemma int_iffD2: assumes h: "\<turnstile> F = G"
  shows "\<turnstile> G \<longrightarrow> F"
  using h[THEN intD] by auto

lemma lift_imp_trans: assumes h1: "\<turnstile> A \<longrightarrow> B"
                         and  h2: "\<turnstile> B \<longrightarrow> C"
                       shows      "\<turnstile> A \<longrightarrow> C"
using h1 h2
by (unfold Valid_def) (auto)

lemma lift_imp_neg: assumes h1: "\<turnstile> A \<longrightarrow> B"
                       shows    "\<turnstile> \<not>B \<longrightarrow> \<not>A"
using h1
by (unfold Valid_def) (auto)

lemma lift_and_com:  "\<turnstile> (A \<and> B) = (B \<and> A)"
by (unfold Valid_def) (auto)


section "Not working"


text{* Turn  @{term "\<turnstile> F = G"} into meta-level rewrite rule  @{term "F \<equiv> G"} *}

(*
  Fix: Cannot get this to work - even by applying rules directly without using tactic - see below
*)
(*
method_setup int_rewrite = 
{*
let 
  fun int_rewrite_tac args ctxt = 
      let val intensional_rews = ProofContext.get_thms ctxt (PureThy.Name "intensional_rews")
      in 
        (Method.METHOD (fn chained_facts => 
           (fn th => 
           Seq.single (rewrite_rule intensional_rews ((th RS thm "inteq_reflection") handle _ => th)))))
      end
in 
  int_rewrite_tac
end
*} "int_unlift tactic lifted to being a method."
*)
(*
lemma assumes H:"\<turnstile> F = G" shows "F \<equiv> G"
proof -
  from H show "F \<equiv> G" by (rule inteq_reflection)
qed
*)

subsubsection {* Flattening *}

text{* Flatting turns \<longrightarrow> into \<Longrightarrow>  and eliminates conjunctions in the
antecedent. E.g. @{term "P \<and> Q \<longrightarrow> (R \<or> S \<longrightarrow> T)"}  becomes   
@{term "\<lbrakk> P; Q; R \<or> S \<rbrakk> \<Longrightarrow> T"}. Flattening can be useful with \emph{intensional} 
lemmas (after unlifting). Naive resolution with mp and conjI may run away because 
of higher-order unification, therefore the code is a little awkward.*}

(* 
 Fix: doesn't works

 Note:  WHY not "apply (rule impI | erule conjE)+" : examples where this run away because
        of higher-order unification
*)


end